extend_eq_top

Mathlib.MeasureTheory.Measure.AddContent

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

← MathLib Explorer

English

If s is not in C, the extended content assigns the value ∞ to s.

Русский

Если S не принадлежит C, то расширенное содержимое приписывает S значение ∞.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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