map_self — Mathlib

English

If f is an isomorphism and φ is strongly Cartesian over f, then φ is an isomorphism.

Русский

Если основание f является изоморфизмом, а φ сильно-картезианский над f, то φ является изоморфизмом.

LaTeX

$$$[IsStronglyCartesian(p,f,\\phi)] \\land IsIso(f) \\Rightarrow IsIso(\\phi).$$$

Lean4

@[simp]
theorem map_self : map p f φ (id_comp f).symm φ = 𝟙 a :=
  by
  subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [id_comp]

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