restrict_congr_set

Mathlib.MeasureTheory.Measure.Restrict

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

English

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

Русский

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

LaTeX

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

Lean4

theorem restrict_congr_set (h : s =ᵐ[μ] t) : μ.restrict s = μ.restrict t :=
  le_antisymm (restrict_mono_ae h.le) (restrict_mono_ae h.symm.le)

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

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

Разделы

Аффилиация

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