inter

Mathlib.MeasureTheory.Measure.Tight

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsTightMeasureSet.inter

English

If S is tight, then S ∩ T is tight for any T.

Русский

Если S плотное, то пересечение S с любым T тоже плотное.

LaTeX

$$IsTightMeasureSet(S) ⇒ IsTightMeasureSet(S ∩ T)$$

Lean4

protected theorem inter (hS : IsTightMeasureSet S) (T : Set (Measure 𝓧)) : IsTightMeasureSet (S ∩ T) :=
  hS.subset inter_subset_left

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

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

Разделы

Аффилиация

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