exists_mem_of_nonempty

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.exists_mem_of_nonempty

English

If α is nonempty, there exists an x ∈ α.

Русский

Если множество α непусто, существует элемент x ∈ α.

LaTeX

$$$[\text{Nonempty } \alpha] \Rightarrow \exists x : \alpha, x \in \mathrm{univ}$$$

Lean4

theorem exists_mem_of_nonempty (α) : ∀ [Nonempty α], ∃ x : α, x ∈ (univ : Set α)
  | ⟨x⟩ => ⟨x, trivial⟩

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

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

Разделы

Аффилиация

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