nonempty_of_sInf_eq_succ

Mathlib.Data.Nat.Lattice

URI: https://scilib.ai/kg/mathlib#Nat.nonempty_of_sInf_eq_succ

English

If sInf s = k + 1 then s ≠ ∅.

Русский

Если sInf s = k+1, то s не пустое.

LaTeX

$$$sInf(s) = k + 1 \Rightarrow s \neq \emptyset$$$

Lean4

theorem nonempty_of_sInf_eq_succ {s : Set ℕ} {k : ℕ} (h : sInf s = k + 1) : s.Nonempty :=
  nonempty_of_pos_sInf (h.symm ▸ succ_pos k : sInf s > 0)

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

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

Разделы

Аффилиация

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