nonempty

Mathlib.Data.Set.Subsingleton

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

English

If a set s is nontrivial, then s is nonempty (there exists an element in s).

Русский

Если множество s не тривиально, то оно непусто (существует элемент множества).

LaTeX

$$(s.Nontrivial) \Rightarrow (\exists x, x \in s)$$

Lean4

protected theorem nonempty (hs : s.Nontrivial) : s.Nonempty :=
  let ⟨x, hx, _⟩ := hs
  ⟨x, hx⟩

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

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

Разделы

Аффилиация

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