isOpen_iff_continuous_mem — Mathlib

English

Let α be a topological space and s ⊆ α. Then s is open iff the map x ↦ (x ∈ s) is continuous.

Русский

Пусть α — топологическое пространство и S ⊆ α. Тогда S открыто тогда, когда отображение x ↦ (x ∈ S) непрерывно.

LaTeX

$$$\\mathrm{IsOpen}(s) \\iff \\mathrm{Continuous}\\bigl(\\lambda x. x \\in s\\bigr)$$$

Lean4

theorem isOpen_iff_continuous_mem {s : Set α} : IsOpen s ↔ Continuous (· ∈ s) :=
  continuous_Prop.symm

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