cardinal_bUnion — Mathlib

English

If S ⊆ ι with #S < c and h: ∀ i hi, s i hi ≤ᶠ[l] t i hi, then ⋃ i ∈ S, s i hi ≤ᶠ[l] ⋃ i ∈ S, t i hi.

Русский

Пусть S ⊆ ι с #S < c и для каждого i ∈ S, hi, s(i, hi) ≤ᶠ[l] t(i, hi). Тогда ⋃ i∈S s(i, hi) ≤ᶠ[l] ⋃ i∈S t(i, hi).

LaTeX

$$$#S < c \\rightarrow (\\forall i \\in S, \\forall hi \\in i, s(i, hi) \\le^l_{\\mathrm{Eventually}} t(i, hi)) \\rightarrow \\bigcup_{i \\in S} s(i, hi) \\le^l_{\\mathrm{Eventually}} \\bigcup_{i \\in S} t(i, hi)$$$

Lean4

theorem cardinal_bUnion {S : Set ι} (hS : #S < c) {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋃ i ∈ S, s i ‹_› ≤ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
  by
  simp only [biUnion_eq_iUnion]
  exact EventuallyLE.cardinal_iUnion hS fun i => h i i.2

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