restrict_biUnion_congr — Mathlib

English

For countable ι, if directed by subset, the restriction equals the iSup of the restrictions.

Русский

Для счетного ι и направленного по подмножеству: ограничение равно iSup ограничений.

LaTeX

$$$[Countable\, ι] \ (Directed (\\subseteq) s) \Rightarrow \mu.restrict (\\bigcup i, s i) = \\bigsup_i \mu.restrict (s i)$$$

Lean4

theorem restrict_biUnion_congr {s : Set ι} {t : ι → Set α} (hc : s.Countable) :
    μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i) :=
  by
  haveI := hc.toEncodable
  simp only [biUnion_eq_iUnion, SetCoe.forall', restrict_iUnion_congr]

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