over_iso_iff — Mathlib

English

For a fixed object X in T and morphism property P with respects-isomorphisms, the property of the hom component of a morphism in Over X is preserved under isomorphisms.

Русский

Для фиксированного объекта X в T и свойства морфизмов P, сохраняющего изоморфизмы, свойство гомоморфизма в Over X сохраняется при изоморфизмах.

LaTeX

$$$P\\text{ over }(X):\\; {\\text{for } f:g:X\\to-}{ } P(f.hom) \\iff P(g.hom)$$$

Lean4

theorem over_iso_iff (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Over X} (e : f ≅ g) : P f.hom ↔ P g.hom :=
  P.comma_iso_iff e

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