instOne

Mathlib.Algebra.Order.UpperLower

URI: https://scilib.ai/kg/mathlib#UpperSet.instOne

English

The unit of the upper-set structure on α is the upper set {x ∈ α | x ≥ 1}.

Русский

Единица структуры верхних множеств над α равна множеству {x ∈ α | x ≥ 1}.

LaTeX

$$$1_{\\text{UpperSet}(\\alpha)} = \\{ x \\in \\alpha : x \\ge 1 \\}$$$

Lean4

@[to_additive]
instance : One (UpperSet α) :=
  ⟨Ici 1⟩

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

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

Разделы

Аффилиация

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