prop_of_epi

Mathlib.CategoryTheory.ObjectProperty.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.prop_of_epi

English

If f: X → Y is an epimorphism and P X holds, then P Y also holds.

Русский

Если f: X → Y — эпиморфизм и P(X) верно, тогда P(Y) тоже верно.

LaTeX

$$$\forall X,Y, f:X\to Y\ [\mathrm{Epi}(f)], P(X) \Rightarrow P(Y).$$$

Lean4

theorem prop_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (hX : P X) : P Y :=
  IsClosedUnderQuotients.prop_of_epi f hX

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru