biSup_measure_Iic — Mathlib

English

For a countable directed cofinal subset s of a Preorder α, the supremum of μ(Iic(x)) over x in s equals μ(univ).

Русский

Для счетного направленного подмножества s, хватающего в любом предодположении α, верхняя грань меры μ(Iic(x)) по x из s равна μ(всё).

LaTeX

$$$\bigsqcup_{x\in s} \mu(Iic(x))$ (в теории меры) = μ(univ).$$

Lean4

theorem biSup_measure_Iic [Preorder α] {s : Set α} (hsc : s.Countable) (hst : ∀ x : α, ∃ y ∈ s, x ≤ y)
    (hdir : DirectedOn (· ≤ ·) s) : ⨆ x ∈ s, μ (Iic x) = μ univ :=
  by
  rw [← measure_biUnion_eq_iSup hsc]
  · congr
    simp only [← bex_def] at hst
    exact iUnion₂_eq_univ_iff.2 hst
  · exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

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