restrict_apply

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any sets s,t and outer measure m, restrict s m t = m(t ∩ s).

Русский

Для любых множеств s,t и внешней меры m выполняется restrict s m t = m(t ∩ s).

LaTeX

$$$ (\restrict\ s\ m)(T) = m(T \cap s) $$$

Lean4

@[simp]
theorem restrict_apply (s t : Set α) (m : OuterMeasure α) : restrict s m t = m (t ∩ s) := by
  simp [restrict, inter_comm t]

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

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

Разделы

Аффилиация

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