biUnion — Mathlib

English

If s.SupIndep of the families g i and every g i' is SupIndep, then the biUnion of the families also is SupIndep.

Русский

Если для каждой i ∈ s семейства g i образуют SupIndep и для каждой i ∈ s все такие SupIndep, то их биобъединение также SupIndep.

LaTeX

$$$(s.biUnion g).SupIndep f$$

Lean4

/-- Bind operation for `SupIndep`. -/
protected theorem biUnion [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.biUnion g).SupIndep f :=
  by
  rw [← sup_eq_biUnion]
  exact hs.sup hg

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