ne_empty

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.ne_empty

English

If a set s is nontrivial, then s is not empty; equivalently, s ≠ ∅.

Русский

Если множество s не тривиально, то оно не пусто; эквивалентно s ≠ ∅.

LaTeX

$$(s.Nontrivial) \Rightarrow (s \neq \emptyset)$$

Lean4

protected theorem ne_empty (hs : s.Nontrivial) : s ≠ ∅ :=
  hs.nonempty.ne_empty

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

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

Разделы

Аффилиация

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