isIso_of_bijective — Mathlib

English

If f: x → y is such that the underlying order-homomorphism is bijective, then f is an isomorphism.

Русский

Если f: x → y таков, что соответствующая отображение порядка конвертуется в биективное отображение, то f является изоморфизмом.

LaTeX

$$$\\\\forall {x,y} \\\\forall f: x \\\\to y,[\\\\text{Bijective}(f^{\\\\mathrm{toOrderHom}}^{\\\\toFun})] \\\Rightarrow \\\\text{IsIso}(f)$$$

Lean4

theorem isIso_of_bijective {x y : SimplexCategory} {f : x ⟶ y} (hf : Function.Bijective f.toOrderHom.toFun) : IsIso f :=
  haveI : IsIso ((forget SimplexCategory).map f) := (isIso_iff_bijective _).mpr hf
  isIso_of_reflects_iso f (forget SimplexCategory)

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