isOpen_iff — Mathlib

English

A set s is open iff every point of s is contained in a basis element contained in s.

Русский

Множество s открыто тогда и только тогда, когда каждый его элемент содержится в элементе базы, который целиком содержится в s.

LaTeX

$$isOpen_iff {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s$$

Lean4

theorem isOpen_iff {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) :
    IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s := by simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

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