Qiso_inv_hom_id — Mathlib

English

For any s ∈ W, the inverse map Qinv s hs is an isomorphism in the localization.

Русский

Для любого 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

@[reassoc (attr := simp)]
theorem Qiso_inv_hom_id {X Y : C} (s : X ⟶ Y) (hs : W s) : Qinv s hs ≫ (Q W).map s = 𝟙 _ :=
  (Qiso s hs).inv_hom_id

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