isoClosure_eq_self — Mathlib

English

If P is closed under isomorphisms, then the iso-closure of P coincides with P itself.

Русский

Если P замкнуто по изоморфизмам, то isoClosure(P) = P.

LaTeX

$$$$ isoClosure(P) = P \quad\text{if } P.\text{IsClosedUnderIsomorphisms}. $$$$

Lean4

theorem isoClosure_eq_self [IsClosedUnderIsomorphisms P] : isoClosure P = P :=
  by
  apply le_antisymm
  · intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_iso P e.symm hY
  · exact le_isoClosure P

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