eq

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq

English

Absolute continuity is preserved under equality: if v = w then v ≪ᵥ w.

Русский

Абсолютная непрерывность сохраняется при равенстве: если v = w, тогда v ≪ᵥ w.

LaTeX

$$Eq v w → v ≪ᵥ w$$

Lean4

theorem eq {w : VectorMeasure α M} (h : v = w) : v ≪ᵥ w := fun _ hs => h.symm ▸ hs

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

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

Разделы

Аффилиация

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