map_sup

Mathlib.MeasureTheory.OuterMeasure.Operations

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

← MathLib Explorer

English

For any f, m, m', map f (m ⊔ m') = map f m ⊔ map f m'.

Русский

Для любой f, m, m' выполняется map f (m ⊔ m') = map f m ⊔ map f m'.

LaTeX

$$$ map\ f\ (m \sqcup m') = (map\ f\ m) \sqcup (map\ f\ m') $$$

Lean4

@[simp]
theorem map_sup {β} (f : α → β) (m m' : OuterMeasure α) : map f (m ⊔ m') = map f m ⊔ map f m' :=
  ext fun s => by simp only [map_apply, sup_apply]

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

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

Разделы

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

Аффилиация

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