restrict_le_self

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any OuterMeasure m on α and any set s ⊆ α, the restricted outer measure restrict s m is less than or equal to m.

Русский

Для любой внешней меры m на α и любого множества s ⊆ α ограниченная мера restrict s m не превосходит m.

LaTeX

$$$ restrict\ s\ m \le m $$$

Lean4

theorem restrict_le_self (m : OuterMeasure α) (s : Set α) : restrict s m ≤ m :=
  map_comap_le _ _

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

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

Разделы

Аффилиация

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