sSup_eq_zero'

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.sSup_eq_zero'

English

The zero-valued supremum characterisation: sSup s = 0 iff s is empty or s = {0}.

Русский

Характеризация нулевой верхней грани: sSup s = 0 тогда и только тогда, когда s пусто или равно {0}.

LaTeX

$$$\mathrm{sSup} s = 0 \iff s = \varnothing \lor s = \{0\}$$$

Lean4

theorem sSup_eq_zero' : sSup s = 0 ↔ s = ∅ ∨ s = {0} :=
  sSup_eq_bot'

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

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

Разделы

Аффилиация

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