English
If μ is inner regular with respect to predicates p and q, then for any U with q(U) we have μ(U) = sup over K ⊆ U of μ(K) under p(K).
Русский
Если μ внутренняя регуляровка по предикатам p, q, тогда для любого U с q(U) выполняется μ(U) = sup{ μ(K) : K ⊆ U, p(K) }.
LaTeX
$$μ U = ⨆ (K) (_ : K ⊆ U) (_ : p K), μ K$$
Lean4
/-- We say that a measure `μ` is *inner regular* with respect to predicates `p q : Set α → Prop`,
if for every `U` such that `q U` and `r < μ U`, there exists a subset `K ⊆ U` satisfying `p K`
of measure greater than `r`.
This definition is used to prove some facts about regular and weakly regular measures without
repeating the proofs. -/
def InnerRegularWRT {α} {_ : MeasurableSpace α} (μ : Measure α) (p q : Set α → Prop) :=
∀ ⦃U⦄, q U → ∀ r < μ U, ∃ K, K ⊆ U ∧ p K ∧ r < μ K
