Q_inverts — Mathlib

English

Symmetry of the RightFractionRel relation: if z1 relates to z2, then z2 relates to z1.

Русский

Симметрия отношения RightFractionRel: если z1 связано z2, то z2 связано z1.

LaTeX

$$$\forall X,Y\,\forall z_1,z_2 \in W.RightFraction X Y, RightFractionRel(z_1,z_2) \Rightarrow RightFractionRel(z_2,z_1)$$$

Lean4

theorem _root_.CategoryTheory.MorphismProperty.Q_inverts : W.IsInvertedBy W.Q := fun _ _ w hw =>
  (Localization.Construction.wIso w hw).isIso_hom

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