instIsIsoQinv — Mathlib

English

For X,Y and s ∈ W, the inverse Qinv s hs is an isomorphism in the localized setting.

Русский

Для X,Y и s ∈ W обратная карта Qinv s hs является изоморфизмом в локализации.

LaTeX

$$$\forall {C} [\text{Category } C] {W} [W.HasLeftCalculusOfFractions] {X Y} (s: X \to Y) (hs: W s), IsIso (Qinv s hs)$$$

Lean4

instance {X Y : C} (s : X ⟶ Y) (hs : W s) : IsIso (Qinv s hs) :=
  (inferInstance : IsIso (Qiso s hs).inv)

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