nhds_basis_closed_balanced — Mathlib

English

There is a basis of neighborhoods of 0 consisting of closed, balanced sets.

Русский

Имеется базис окрестностей нуля, состоящий из замкнутых сбалансированных множеств.

LaTeX

$$(nhds 0).HasBasis (fun s => And (s ∈ nhds 0) (And (IsClosed s) (Balanced 𝕜 s))) id$$

Lean4

theorem nhds_basis_closed_balanced [RegularSpace E] :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ IsClosed s ∧ Balanced 𝕜 s) id :=
  by
  refine (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩
  refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩
  exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩

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