measureCaratheodory_eq

Mathlib.MeasureTheory.OuterMeasure.OfAddContent

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

← MathLib Explorer

English

For s ∈ C, the measureCaratheodory equals m on s.

Русский

Для s ∈ C мера measureCaratheodory совпадает с m на s.

LaTeX

$$$s \\in C \\Rightarrow m.measureCaratheodory hC m\\_sigma\\_subadd s = m s.$$$

Lean4

theorem measureCaratheodory_eq (m : AddContent C) (hC : IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive)
    (hs : s ∈ C) : m.measureCaratheodory hC m_sigma_subadd s = m s :=
  m.inducedOuterMeasure_eq hC m_sigma_subadd hs

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

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

Разделы

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

Аффилиация

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