isoOfIsoLift_hom_inv_id — Mathlib

English

If f : R ⟶ S and φ : a ≅ b with p.IsHomLift f.hom φ.hom, then f ≫ (isoOfIsoLift p f φ).inv = 1_R.

Русский

Если f : R ⟶ S и φ : a ≅ b с p.IsHomLift f.hom φ.hom, то f затем inv(isoOfIsoLift p f φ) равно единице на R.

LaTeX

$$$\forall {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b)\ [p.IsHomLift f.hom φ.hom],\ f \circ (isoOfIsoLift p f φ).inv = 𝟙_R$$$

Lean4

@[simp]
theorem isoOfIsoLift_hom_inv_id (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] : f ≫ (isoOfIsoLift p f φ).inv = 𝟙 R :=
  (isoOfIsoLift p f φ).hom_inv_id

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