extend_eq

Mathlib.MeasureTheory.Measure.AddContent

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AddContent.extend_eq

English

If s belongs to C, then the extended content agrees with m on s.

Русский

Если s ∈ C, то расширенное содержимое совпадает с m на s.

LaTeX

$$$(m.\extend\,hC)(s) = m(s) \quad \text{если } s \in C$$$

Lean4

protected theorem extend_eq (hC : IsSetSemiring C) (m : AddContent C) (hs : s ∈ C) : m.extend hC s = m s := by
  rwa [m.extend_eq_extend, extend_eq]

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

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

Разделы

Аффилиация

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