innerRegularWRT_isCompact_closure_of_univ

English

If for every ε>0 there exists K with IsCompact(closure K) and μ(K^c) < ε, then μ is inner regular with respect to closure of compact sets and closed sets.

Русский

Если для каждого ε>0 существует K с IsCompact(closure K) и μ(K^c)<ε, то μ — внутренняя регулярность по closures и замкнутым множествам.

LaTeX

$$$\\forall ε>0,\\exists K:\\ IsCompact(\\overline{K}) \\wedge μ(K^{c})<ε \\Rightarrow μ.InnerRegularWRT (IsCompact \\circ closure) IsClosed.$$$

Lean4

theorem innerRegularWRT_isCompact_closure_of_univ [TopologicalSpace α]
    (hμ : ∀ ε, 0 < ε → ∃ K, IsCompact (closure K) ∧ μ (Kᶜ) < ε) : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
  by
  refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ
  have : IsCompact (closure s ∩ t) := hs.inter_right ht
  refine this.of_isClosed_subset isClosed_closure ?_
  refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
  rw [IsClosed.closure_eq ht]

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