exists_isHahnDecomposition — Mathlib

English

For finite measures μ and ν, there exists a set s that forms a Hahn decomposition for (μ, ν).

Русский

Для конечных мер μ и ν существует множество s, образующее разложение Хана для (μ,ν).

LaTeX

$$$$\exists s:\text{Set},\text{IsHahnDecomposition}(μ,ν,s).$$$$

Lean4

theorem exists_isHahnDecomposition (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    ∃ s : Set α, IsHahnDecomposition μ ν s :=
  by
  obtain ⟨s, hs, h₁, h₂⟩ := hahn_decomposition ν μ
  refine ⟨s, hs, ?_, ?_⟩
  all_goals
    rw [Measure.le_iff]
    intros
    simp [*]

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