Module docstring
{}
Subtype.ext
theorem
: ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
Full source
@[ext]
protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
| ⟨_, _⟩, ⟨_, _⟩, rfl => rflInformal description
For any two elements $a_1$ and $a_2$ of the subtype $\{x \mid p(x)\}$, if their underlying values in $\alpha$ are equal (i.e., $(a_1 : \alpha) = (a_2 : \alpha)$), then $a_1 = a_2$ as elements of the subtype.
Subtype.forall
theorem
{q : { a // p a } → Prop} : (∀ x, q x) ↔ ∀ a b, q ⟨a, b⟩
Full source
@[simp]
protected theorem «forall» {q : { a // p a } → Prop} : (∀ x, q x) ↔ ∀ a b, q ⟨a, b⟩ :=
⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩Informal description
For any predicate $q$ defined on the subtype $\{x \mid p(x)\}$, the universal quantification $(\forall x, q(x))$ holds if and only if for every element $a$ of the base type and every proof $b$ that $p(a)$ holds, the predicate $q$ holds on the element $\langle a, b \rangle$ of the subtype.
Subtype.exists
theorem
{q : { a // p a } → Prop} : (Exists fun x => q x) ↔ Exists fun a => Exists fun b => q ⟨a, b⟩
Full source
@[simp]
protected theorem «exists» {q : { a // p a } → Prop} :
(Exists fun x => q x) ↔ Exists fun a => Exists fun b => q ⟨a, b⟩ :=
⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩Informal description
For any predicate $q$ defined on the subtype $\{x \mid p(x)\}$, the existential quantification $(\exists x, q(x))$ holds if and only if there exists an element $a$ of the base type and a proof $b$ that $p(a)$ holds such that $q$ holds on the element $\langle a, b \rangle$ of the subtype.