mono_f₁₃

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Square.IsPullback.mono_f₁₃

English

If sq is a Pullback and f24 is mono, then f13 is mono.

Русский

Если sq — Pullback и f24 моно, то f13 моно.

LaTeX

$$[Mono sq.f24] ⇒ [Mono sq.f13]$$

Lean4

theorem mono_f₁₃ [Mono sq.f₂₄] : Mono sq.f₁₃ :=
  (MorphismProperty.monomorphisms C).of_isPullback h (by assumption)

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

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

Разделы

Аффилиация

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