ae_of_ae_restrict_of_ae_restrict_compl

English

If s ⊆ t and p holds almost everywhere on μ.restrict t, then p holds almost everywhere on μ.restrict s.

Русский

Если s ⊆ t и p выполняется почти наверху μ|_t, тогда p выполняется почти наверху μ|_s.

LaTeX

$$$s \subseteq t \Rightarrow (\forall^\mathrm{a.e.}_{x} \ p(x) \text{ w.r.t. } μ|_t) \Rightarrow (\forall^\mathrm{a.e.}_{x} \ p(x) \text{ w.r.t. } μ|_s).$$$

Lean4

theorem ae_of_ae_restrict_of_ae_restrict_compl (t : Set α) {p : α → Prop} (ht : ∀ᵐ x ∂μ.restrict t, p x)
    (htc : ∀ᵐ x ∂μ.restrict tᶜ, p x) : ∀ᵐ x ∂μ, p x :=
  nonpos_iff_eq_zero.1 <|
    calc
      μ {x | ¬p x} ≤ μ ({x | ¬p x} ∩ t) + μ ({x | ¬p x} ∩ tᶜ) := measure_le_inter_add_diff _ _ _
      _ ≤ μ.restrict t {x | ¬p x} + μ.restrict tᶜ {x | ¬p x} :=
        (add_le_add (le_restrict_apply _ _) (le_restrict_apply _ _))
      _ = 0 := by rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]

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