mem_mk

Mathlib.Topology.Sets.Opens

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

English

For elements x of α, x belongs to the open set ⟨U,h⟩ iff x ∈ U.

Русский

Для элемента x ⊆ α выполнено: x ∈ ⟨U,h⟩ ⇔ x ∈ U.

LaTeX

$$$x \in (\langle U,h\rangle : Opens α) \iff x \in U$.$$

Lean4

@[simp]
theorem mem_mk {x : α} {U : Set α} {h : IsOpen U} : x ∈ mk U h ↔ x ∈ U :=
  Iff.rfl

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

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

Разделы

Аффилиация

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