exists_closure_subset — Mathlib

English

Given a topological basis B and a point x with s ∈ nhds x, there exists a basis element t ∈ B such that x ∈ t and closure t ⊆ s.

Русский

Пусть B — топологический базис, для точки x и s ∈ nhds x существует элемент t ∈ B с x ∈ t и closure t ⊆ s.

LaTeX

$$$\forall {B} (hB : IsTopologicalBasis B) {x} {s} (h : s \in 𝓝 x), \exists t \in B, x \in t ∧ closure t ⊆ s$$$

Lean4

theorem exists_closure_subset {B : Set (Set X)} (hB : IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ 𝓝 x) :
    ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s := by
  simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

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