English
A subtype of a subtype is equivalent to the subtype of elements with an existential witness: { x : α // p x ∧ q x } ⇔ { a : α // ∃ h, q ⟨a, h⟩ } (with appropriate p, q).\nThe exact statement expresses equivalence between { x : Subtype p // q x.1 } and { a : α // ∃ h : p a, q ⟨a, h⟩ }.
Русский
Подтип подтипа эквивалентен подтипу элементов, удовлетворяющих комбинации предикатов; то есть существует биекция между { x : α | p x, q x } и { a : α | ∃ h, q ⟨a, h⟩ }.
LaTeX
$$$\\{ x : \\text{Subtype } p \\;\\mid\\; q x.1 \\} \\simeq \\{ a : \\alpha \\;\\mid\\; \\exists h : p a, q \\langle a, h \\rangle \\}$$$
Lean4
/-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
version allows the “inner” predicate to depend on `h : p a`. -/
@[simps]
def subtypeSubtypeEquivSubtypeExists (p : α → Prop) (q : Subtype p → Prop) :
Subtype q ≃ { a : α // ∃ h : p a, q ⟨a, h⟩ } :=
⟨fun a =>
⟨a.1, a.1.2, by
rcases a with ⟨⟨a, hap⟩, haq⟩
exact haq⟩,
fun a => ⟨⟨a, a.2.fst⟩, a.2.snd⟩, fun ⟨⟨_, _⟩, _⟩ => rfl, fun ⟨_, _, _⟩ => rfl⟩
