English
From a base-point preserving equivalence e: α ≃ β between pointed types, construct an isomorphism of pointed types α ≅ β.
Русский
Из эквивалентности, сохраняющей точку, между заданными точками α и β строится изоморфизм точек α ≅ β.
LaTeX
$$$\mathrm{Pointed.Iso.mk}(e : α \simeq β,\; h : e(α.point) = β.point) : α \cong β.$$$
Lean4
/-- Constructs an isomorphism between pointed types from an equivalence that preserves the point
between them. -/
@[simps]
def mk {α β : Pointed} (e : α ≃ β) (he : e α.point = β.point) : α ≅ β
where
hom := ⟨e, he⟩
inv := ⟨e.symm, e.symm_apply_eq.2 he.symm⟩
hom_inv_id := Pointed.Hom.ext e.symm_comp_self
inv_hom_id := Pointed.Hom.ext e.self_comp_symm
