exists_isCompl_positive_negative — Mathlib

English

There exist measurable i, j such that i and j are complements, and s has compatible bounds on both i and its complement and j and its complement.

Русский

Существуют измеримые i, j такие, что i и j являются дополнениями, и s удовлетворяет соответствующим ограничениям на i и i^c, а также на j и j^c.

LaTeX

$$$\exists i,j \ {\text{MeasurableSet } i, \text{MeasurableSet } j \;\land 0 \le[i] s \land s \le[i^c] 0 \land 0 \le[j] s \land s \le[j^c] 0 \land IsCompl i j}$$$

Lean4

/-- **The Hahn decomposition theorem**: Given a signed measure `s`, there exist
complement measurable sets `i` and `j` such that `i` is positive, `j` is negative. -/
theorem exists_isCompl_positive_negative (s : SignedMeasure α) :
    ∃ i j : Set α, MeasurableSet i ∧ 0 ≤[i] s ∧ MeasurableSet j ∧ s ≤[j] 0 ∧ IsCompl i j :=
  let ⟨i, hi₁, hi₂, hi₃⟩ := exists_compl_positive_negative s
  ⟨i, iᶜ, hi₁, hi₂, hi₁.compl, hi₃, isCompl_compl⟩

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