essSup_eq — Mathlib

English

For IdentDistrib f g μ ν, the a.e. equality of sets transfers from f to g.

Русский

Для IdentDistrib f g μ ν переходят по a.e. равенству множеств от f к g.

LaTeX

$$$ae_snd (h) (pmeas) (hp) : (∀ᵐ x ∂ν, p (g x))$$$

Lean4

theorem essSup_eq [ConditionallyCompleteLinearOrder γ] [TopologicalSpace γ] [OpensMeasurableSpace γ]
    [OrderClosedTopology γ] (h : IdentDistrib f g μ ν) : essSup f μ = essSup g ν :=
  by
  have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a => h.measure_mem_eq measurableSet_Ioi
  simp_rw [essSup_eq_sInf, I]

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