map_apply

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any function f : α → β, OuterMeasure m on α, and set S ⊆ β, the value is (map f m)(S) = m(f^{-1}(S)).

Русский

Для любой функции f: α → β, внешней меры m на α и множества S ⊆ β имеет место (map f m)(S) = m(f^{-1}(S)).

LaTeX

$$$ (map f m) S = m (f^{-1}(S)) $$$

Lean4

@[simp]
theorem map_apply {β} (f : α → β) (m : OuterMeasure α) (s : Set β) : map f m s = m (f ⁻¹' s) :=
  rfl

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

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

Разделы

Аффилиация

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