restrict_mono_ae

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.restrict_mono_ae

English

If s and t are almost everywhere equal with respect to μ, then μ|s = μ|t.

Русский

Если множества s и t равны почти везде относительно μ, то μ|s = μ|t.

LaTeX

$$$s =_{μ} t \Rightarrow μ|s = μ|t.$$$

Lean4

theorem restrict_mono_ae (h : s ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t :=
  restrict_mono' h (le_refl μ)

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

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

Разделы

Аффилиация

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