coe_eq_empty

Mathlib.Topology.Sets.Opens

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

English

For any open set U, (U : Set α) = ∅ if and only if U = ⊥.

Русский

Для любого открытого множества U верно: множество U как подмножество пусто тогда и только тогда, когда U = ⊥.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_eq_empty {U : Opens α} : (U : Set α) = ∅ ↔ U = ⊥ :=
  SetLike.coe_injective.eq_iff' rfl

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

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

Разделы

Аффилиация

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