llp_of_isIso — Mathlib

English

Let T be a morphism property on C. If i: A → B is an isomorphism, then i has the left lifting property with respect to T; i.e., T.llp i holds.

Русский

Пусть T — свойство морфизмов в C. Если i: A → B является изоморфизмом, то i имеет левое прокалывающее свойство по отношению к T; то есть T.llp i выполняется.

LaTeX

$$$\forall A,B\, (i: A \to B), \ \mathrm{IsIso}(i) \Rightarrow T.llp(i)$$$

Lean4

theorem llp_of_isIso {A B : C} (i : A ⟶ B) [IsIso i] : T.llp i := fun _ _ _ _ ↦ inferInstance

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