English
For any μ, if a certain covering by closures of compact sets exists on the universe, μ is inner regular with respect to closure of compact sets.
Русский
Если существует покрытие по замыканиям компактных множеств на всём пространстве, то μ — внутренняя регулярность по замыканиям компактных множеств.
LaTeX
$$$\\mu.InnerRegularWRT (IsCompact \\circ closure) IsClosed$$$
Lean4
theorem innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure [TopologicalSpace α] [R1Space α] :
μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
by
constructor <;> intro h A hA r hr
· obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
refine ⟨K, hK1, ?_, hK4⟩
simp only [Function.comp_apply]
exact hK2.closure
· obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
· simpa only [isClosed_closure, and_true]
· exact hK3.trans_le (measure_mono subset_closure)
