compl — Mathlib

English

If (μ, ν) has a Hahn decomposition on s, then swapping the roles yields a Hahn decomposition on s^c with reversed inequality directions.

Русский

Если есть разложение Хана на множестве s, то переход к противоположному множеству s^c образует разложение на ν, μ с обратными неравенствами.

LaTeX

$$$$\text{IsHahnDecomposition}(μ,ν,s) \Rightarrow \text{IsHahnDecomposition}(ν,μ, s^c).$$$$

Lean4

theorem compl {μ ν : Measure α} {s : Set α} (h : IsHahnDecomposition μ ν s) : IsHahnDecomposition ν μ sᶜ
    where
  measurableSet := h.measurableSet.compl
  le_on := h.ge_on_compl
  ge_on_compl := by simpa using h.le_on

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