measure_congr

Mathlib.MeasureTheory.OuterMeasure.AE

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

← MathLib Explorer

English

If s =ᵐ[μ] t, then μ s = μ t.

Русский

Если s равняется t почти по μ, то μ s = μ t.

LaTeX

$$$(s =_{\mathrm{ae}}^{\mu} t) \Rightarrow \mu s = \mu t$$$

Lean4

/-- If two sets are equal modulo a set of measure zero, then `μ s = μ t`. -/
theorem measure_congr (H : s =ᵐ[μ] t) : μ s = μ t :=
  le_antisymm H.le.measure_le H.symm.le.measure_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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