union_ae_eq_right_iff_ae_subset — Mathlib

English

If s is almost contained in t and μ(t) ≤ μ(s) and s is null-measurable with μ(t) ≠ ∞, then s and t are equal μ-almost everywhere.

Русский

Если s почти содержится в t и μ(t) ≤ μ(s), и s является нулево измеримым относительно μ, а μ(t) не бесконечна, то s и t равны μ-почти где-нибудь.

LaTeX

$$$ (s \leq^{\mu}_{\mathrm{a.e.}} t) \land (\mu t \le \mu s) \land (\text{NullMeasurableSet}(s, \mu)) \land (\mu t \neq \infty) \Rightarrow (s =^{\mu}_{\mathrm{a.e.}} t) $$$

Lean4

@[simp]
theorem union_ae_eq_right_iff_ae_subset : (s ∪ t : Set α) =ᵐ[μ] t ↔ s ≤ᵐ[μ] t := by
  rw [union_comm, union_ae_eq_left_iff_ae_subset]

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