ae_eq_of_ae_subset_of_measure_ge — Mathlib

English

If s ⊆ t, μ t ≤ μ s, μ t ≠ ∞, and s is null-measurable with respect to μ, then s and t are μ-almost equal.

Русский

Если s ⊆ t, μ t ≤ μ s, μ t ≠ ∞ и s является нулево измеримым относительно μ, то s и t равны μ-почти.

LaTeX

$$$ (s \subseteq t) \land (μ t ≤ μ s) \land (NullMeasurableSet(s, μ)) \land (μ t \neq ∞) \Rightarrow (s =^{\mu}_{\mathrm{a.e.}} t) $$$

Lean4

theorem ae_eq_of_ae_subset_of_measure_ge (h₁ : s ≤ᵐ[μ] t) (h₂ : μ t ≤ μ s) (hsm : NullMeasurableSet s μ)
    (ht : μ t ≠ ∞) : s =ᵐ[μ] t :=
  by
  refine eventuallyLE_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr ?_⟩
  replace h₂ : μ t = μ s := h₂.antisymm (measure_mono_ae h₁)
  replace ht : μ s ≠ ∞ := h₂ ▸ ht
  rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]

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