source
theorem Subtype.ext {α : Sort u} {p : α → Prop} {a1 a2 : { x : α // p x }} :
a1.val = a2.val → a1 = a2
source
theorem Subtype.ext_iff {α : Sort u} {p : α → Prop} {a1 a2 : { x : α // p x }} :
a1 = a2 ↔ a1.val = a2.val
source
@[simp]
theorem Subtype.forall {α : Sort u} {p : α → Prop} {q : { a : α // p a } → Prop} :
(∀ (x : { a : α // p a }), q x) ↔ ∀ (a : α) (b : p a), q ⟨a, b⟩
source
@[simp]
theorem Subtype.exists {α : Sort u} {p : α → Prop} {q : { a : α // p a } → Prop} :
(∃ (x : { a : α // p a }), q x) ↔ ∃ (a : α), ∃ (b : p a), q ⟨a, b⟩