measure_diff_biUnion

Mathlib.MeasureTheory.Covering.VitaliFamily

URI: https://scilib.ai/kg/mathlib#VitaliFamily.FineSubfamilyOn.measure_diff_biUnion

English

The leftover part of s after removing the union of all covering sets has measure zero.

Русский

Оставшаяся часть s после вычитания объединения всех покрытий имеет меру нуль.

LaTeX

$$$\\mu\\Bigl(s\\setminus\\bigcup_{p\\in h.index} h.covering(p)\\Bigr)=0.$$$

Lean4

theorem measure_diff_biUnion : μ (s \ ⋃ p ∈ h.index, h.covering p) = 0 :=
  h.exists_disjoint_covering_ae.choose_spec.2.2.2

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

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

Разделы

Аффилиация

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