isIso_of_isIso — Mathlib

English

If f.τ1, f.τ2, f.τ3 are all isomorphisms, then f is an isomorphism.

Русский

Если f.τ1, f.τ2 и f.τ3 являются изоморфизмами, то собственно f является изоморфизмом.

LaTeX

$$$$ (\\text{IsIso}(f.\\tau_1) \\wedge \\text{IsIso}(f.\\tau_2) \\wedge \\text{IsIso}(f.\\tau_3)) \\Rightarrow \\text{IsIso}(f). $$$$

Lean4

theorem isIso_of_isIso (f : S₁ ⟶ S₂) [IsIso f.τ₁] [IsIso f.τ₂] [IsIso f.τ₃] : IsIso f :=
  (isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃)).isIso_hom

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