English
If p is preserved under intersections with sets q, and sets satisfying p cover space arbitrarily well, then μ is inner regular with respect to p and q.
Русский
Если предикат p сохраняется при пересечении с множествами, удовлетворяющими q, и такие множества образуют пространство, то μ является внутренне регулярной относительно p и q.
LaTeX
$$$(\\forall A,B)(pA \\land qB \\Rightarrow p(A\\cap B)) \\Rightarrow (\\forall \\varepsilon>0, \\exists K: pK \\land μ(K^{c})<ε) \\Rightarrow μ.InnerRegularWRT p q.$$$
Lean4
theorem innerRegularWRT_isCompact_closure_iff [TopologicalSpace α] [R1Space α] :
μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed :=
by
constructor <;> intro h A hA r hr
· rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
exact ⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩
· rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
· simpa only [closure_closure, Function.comp_apply] using hK2.closure
· exact hK3.trans_le (measure_mono subset_closure)
