sSup_mem_of_nonempty_of_lt_top

Mathlib.Data.ENat.Lattice

URI: https://scilib.ai/kg/mathlib#ENat.sSup_mem_of_nonempty_of_lt_top

English

If ι is empty, then ⨅ i, (f i : ℕ∞) = ⊤.

Русский

Если индексный тип пуст, то ⨅ i, (f i : ℕ∞) = ⊤.

LaTeX

$$$[IsEmpty \iota] \;: \; \inf_i (f(i) : \mathbb{N}_\infty) = \top$$$

Lean4

theorem sSup_mem_of_nonempty_of_lt_top [Nonempty s] (hs' : sSup s < ⊤) : sSup s ∈ s :=
  Nonempty.csSup_mem .of_subtype (finite_of_sSup_lt_top hs')

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

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

Разделы

Аффилиация

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