disjointed_set_eq

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq

English

The underlying set of a disjointed FiniteSpanningSetsIn equals the set of the original S.

Русский

Взятие disjointed не меняет исходное множество S.

LaTeX

$$$S\text{ disjointed}.set = disjointed S.set$$$

Lean4

theorem disjointed_set_eq {μ : Measure α} (S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}) :
    S.disjointed.set = disjointed S.set :=
  rfl

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

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

Разделы

Аффилиация

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