rlp_of_isIso — Mathlib

English

Let T be a morphism property on C. If f: X → Y is an isomorphism, then f has the right lifting property with respect to T; i.e., T.rlp f holds.

Русский

Пусть T — свойство морфизмов на C. Если f: X → Y является изоморфизмом, то f обладает правым заполнением по отношению к T; то есть T.rlp f выполняется.

LaTeX

$$$\forall X,Y\, (f: X \to Y), \ [\mathrm{IsIso}(f)] \Rightarrow T.rlp(f)$$$

Lean4

theorem rlp_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] : T.rlp f := fun _ _ _ _ ↦ inferInstance

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