of_eq_top

Mathlib.CategoryTheory.MorphismProperty.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.of_eq_top

English

If P = ⊤ as a MorphismProperty, then P f holds for all arrows f: X ⟶ Y.

Русский

Если P = ⊤, то ∀ стрелки f: X → Y выполняется P f.

LaTeX

$$$P = \\top \\Rightarrow \\forall f, P(f).$$$

Lean4

theorem of_eq_top {P : MorphismProperty C} (h : P = ⊤) {X Y : C} (f : X ⟶ Y) : P f := by simp [h]

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

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

Разделы

Аффилиация

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