isOpen_iff_forall_mem_open — Mathlib

English

IsOpen s is equivalent to every point x in s having an open neighborhood t with t ⊆ s.

Русский

IsOpen s эквивалентно тому, что для каждого x ∈ s существует открытое окрестность t с t ⊆ s.

LaTeX

$$$ IsOpen(s) \iff \forall x\in s, \exists t, t \subseteq s \land IsOpen(t) \land x \in t$$$

Lean4

theorem isOpen_iff_forall_mem_open : IsOpen s ↔ ∀ x ∈ s, ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t :=
  by
  rw [← subset_interior_iff_isOpen]
  simp only [subset_def, mem_interior]

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