nonempty_coe

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.nonempty_coe

English

For an open set U, the underlying set U is nonempty iff there exists x ∈ U.

Русский

Для открытого множества U подмножество U непусто тогда, когда существует x ∈ U.

LaTeX

$$$(U : Set α).Nonempty \iff \exists x, x \in U$.$$

Lean4

protected theorem nonempty_coe {U : Opens α} : (U : Set α).Nonempty ↔ ∃ x, x ∈ U :=
  Iff.rfl

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

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

Разделы

Аффилиация

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