isTopologicalBasis_isOpen_lt_top — Mathlib

English

Same as above: the collection of finite-measure open sets is a basis for the topology.

Русский

Та же самая база: коллекция открытых множеств с конечной мерой образует базис топологии.

LaTeX

$$TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ∞}$$

Lean4

protected theorem isTopologicalBasis_isOpen_lt_top [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] :
    TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ∞} :=
  by
  refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds (fun s hs => hs.1) ?_
  intro x s xs hs
  rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩
  refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩
  exact measure_mono inter_subset_left

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