zero_caratheodory

Mathlib.MeasureTheory.OuterMeasure.Caratheodory

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.zero_caratheodory

English

The Carathéodory structure of the zero outer measure is the top

Русский

Структура карatheодory для нулевой внешней меры равна вершине (верх).

LaTeX

$$0 : OuterMeasure α).caratheodory = ⊤$$

Lean4

@[simp]
theorem zero_caratheodory : (0 : OuterMeasure α).caratheodory = ⊤ :=
  top_unique fun _ _ _ => (add_zero _).symm

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

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

Разделы

Аффилиация

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