ae_eq_of_ae_eq_trim

Mathlib.MeasureTheory.Measure.Trim

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ae_eq_of_ae_eq_trim

English

If f1 =ᵐ[μ.trim hm] f2, then f1 =ᵐ[μ] f2.

Русский

Если f1 =ᵐ[μ.trim hm] f2, то f1 =ᵐ[μ] f2.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru