union

Mathlib.MeasureTheory.Measure.Tight

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

← MathLib Explorer

English

If S and T are tight, then their union S ∪ T is tight.

Русский

Если два множества мер плотны, то их объединение плотное.

LaTeX

$$IsTightMeasureSet(S) ∧ IsTightMeasureSet(T) ⇒ IsTightMeasureSet(S ∪ T)$$

Lean4

protected theorem union (hS : IsTightMeasureSet S) (hT : IsTightMeasureSet T) : IsTightMeasureSet (S ∪ T) :=
  by
  rw [IsTightMeasureSet, iSup_union]
  convert Tendsto.sup_nhds hS hT
  simp

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

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

Разделы

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

Аффилиация

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