English
If predicate p is preserved under intersections with q and the complement measure can be made arbitrarily small on complements, μ 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)) \\land (\\forall ε>0, ∃ K, pK \\land μ(K^{c})<ε) \\Rightarrow μ.InnerRegularWRT p q.$$$
Lean4
/-- If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
satisfying `p` cover the space arbitrarily well, then `μ` is inner regular with respect to
predicates `p` and `q`.
-/
theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
(hμ : ∀ ε, 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) : μ.InnerRegularWRT p q :=
by
intro A hA r hr
obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r :=
by
obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
· refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
simp only [diff_inter_self_eq_diff, mem_diff, mem_compl_iff, and_imp, imp_self, imp_true_iff]
refine ⟨K, hK_subset, hK, ?_⟩
have h_lt' : μ A - μ K < μ A - r := le_measure_diff.trans_lt h_lt
exact lt_of_tsub_lt_tsub_left h_lt'
