subtypeUnivEquiv — Mathlib

English

If p holds for all x, then Subtype p is equivalent to α.

Русский

Если p верна для всех x, то подтип p эквивалентен исходному типу α.

LaTeX

$$$(\\forall x, p x) \\Rightarrow \\text{Subtype } p \\simeq \\alpha$$$

Lean4

/-- If a proposition holds for all elements, then the subtype is
equivalent to the original type. -/
@[simps apply symm_apply]
def subtypeUnivEquiv {α} {p : α → Prop} (h : ∀ x, p x) : Subtype p ≃ α :=
  ⟨fun x => x, fun x => ⟨x, h x⟩, fun _ => Subtype.eq rfl, fun _ => rfl⟩

Похожие утверждения