iso_inv_snd — Mathlib

English

The inverse of the product iso composed with map sends the second projection to the original second projection.

Русский

Обратное от изоморфизма произведения в композиции с отображением отправляет вторую проекцию к исходной второй проекции.

LaTeX

$$$(\mathrm{PreservesLimitPair.iso} G X Y).inv \;\gg\; G.map(\text{prod.snd}) = prod.snd$$$

Lean4

@[simp, reassoc]
theorem iso_inv_snd : (PreservesLimitPair.iso G X Y).inv ≫ G.map prod.snd = prod.snd :=
  by
  rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]
  simp

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