instNontrivialOfNonempty

Mathlib.Topology.Sets.Opens

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

English

For U in Opens α, (U : Set α) = ∅ iff U = ⊥.

Русский

Для открытого множества U в Opens α выполняется (U : Set α) = ∅ тогда и только тогда, когда U = ⊥.

LaTeX

$$$ (U : Set α) = \emptyset \iff U = ⊥ $$$

Lean4

instance [Nonempty α] : Nontrivial (Opens α) where exists_pair_ne := ⟨⊥, ⊤, mt coe_inj.2 empty_ne_univ⟩

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

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

Разделы

Аффилиация

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