essSup_mono_measure'

Mathlib.MeasureTheory.Function.EssSup

URI: https://scilib.ai/kg/mathlib#essSup_mono_measure'

← MathLib Explorer

English

If ν ≤ μ, then essSup f ν ≤ essSup f μ.

Русский

Если ν ≤ μ, тогда essSup f ν ≤ essSup f μ.

LaTeX

$$essSup f ν ≤ essSup f μ$$

Lean4

theorem essSup_mono_measure' {α : Type*} {β : Type*} {_ : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
    [CompleteLattice β] {f : α → β} (hμν : ν ≤ μ) : essSup f ν ≤ essSup f μ :=
  essSup_mono_measure (Measure.absolutelyContinuous_of_le hμν)

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

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

Разделы

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

Аффилиация

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