ext

Mathlib.MeasureTheory.Measure.AddContent

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

English

Two AddContent objects are equal if they agree on all sets.

Русский

Два объекта AddContent равны, если совпадают на всех множествах.

LaTeX

$$m = m' ↔ ∀ s, m s = m' s$$

Lean4

@[ext]
protected theorem ext (h : ∀ s, m s = m' s) : m = m' :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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