inr_iso_inv — Mathlib

English

If the pullback comparison map is iso, then the pullback is preserved.

Русский

Если отображение сравнения притяжения является изоморфизмом, то притяжение сохраняется.

LaTeX

$$$IsIso( pullbackComparison G f g )$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_iso_inv : G.map (pushout.inr _ _) ≫ (PreservesPushout.iso G f g).inv = pushout.inr _ _ := by
  simp [PreservesPushout.iso, Iso.comp_inv_eq]

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