ae_le_of_ae_le_trim — Mathlib

English

If f1 ≤ᵐ[μ.trim hm] f2 and E is a linear ordered type, then f1 ≤ᵐ[μ] f2.

Русский

Если f1 ≤ᵐ[μ.trim hm] f2 и E упорядочиваемый по линейному порядку, то f1 ≤ᵐ[μ] f2.

LaTeX

$$$f_1 \\le^{\\mathrm{a.e.}}_{μ.trim hm} f_2 \\Rightarrow f_1 \\le^{\\mathrm{a.e.}}_{μ} f_2.$$$

Lean4

theorem ae_le_of_ae_le_trim {E} [LE E] {hm : m ≤ m0} {f₁ f₂ : α → E} (h12 : f₁ ≤ᵐ[μ.trim hm] f₂) : f₁ ≤ᵐ[μ] f₂ :=
  measure_eq_zero_of_trim_eq_zero hm h12

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