prop_of_mono

Mathlib.CategoryTheory.ObjectProperty.EpiMono

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

English

If P is closed under subobjects and f: X → Y is mono with P Y, then P X.

Русский

Если P замкнуто по подпредикатам и f: X → Y моно, и P(Y) истинно, то P(X).

LaTeX

$$$$ [P.IsClosedUnderSubobjects] \land f: X \to Y \text{ mono} \land P(Y) \Rightarrow P(X). $$$$

Lean4

theorem prop_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (hY : P Y) : P X :=
  IsClosedUnderSubobjects.prop_of_mono f hY

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

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

Разделы

Аффилиация

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