of_isTerminal — Mathlib

English

If C has a terminal object X, then C is filtered.

Русский

Если в C существует терминальный объект X, то C является фильтрованной.

LaTeX

$$$\\exists X\\;\\operatorname{IsTerminal}(X) \\Rightarrow \\operatorname{IsFiltered}(C).$$$

Lean4

theorem of_isTerminal {X : C} (h : IsTerminal X) : IsFiltered C :=
  of_cocone_nonempty.{v} _ fun {_} _ _ _ => ⟨⟨X, ⟨fun _ => h.from _, fun _ _ _ => h.hom_ext _ _⟩⟩⟩

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