nonempty

Mathlib.Data.Set.Finite.Basic

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

English

Any infinite set is nonempty.

Русский

Любое бесконечное множество непусто.

LaTeX

$$$\exists^\\infty x\, (x \in s) \Rightarrow s \neq \varnothing$$$

Lean4

protected theorem nonempty {s : Set α} (h : s.Infinite) : s.Nonempty :=
  nonempty_iff_ne_empty.2 <| by
    rintro rfl
    exact h finite_empty

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

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

Разделы

Аффилиация

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