instNonempty

Mathlib.Order.Zorn

URI: https://scilib.ai/kg/mathlib#Flag.instNonempty

English

There exists at least one flag; the flag type is nonempty.

Русский

Существует хотя бы один флаг; множество флагов не пусто.

LaTeX

$$$$\text{Nonempty}(Flag\alpha).$$$$

Lean4

instance : Nonempty (Flag α) :=
  ⟨.ofIsMaxChain _ maxChain_spec⟩

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

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

Разделы

Аффилиация

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