cardinal_bUnion — Mathlib

English

If S ⊆ ι has #S < c and ∀ 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, s(i, hi) =^l_{\\mathrm{Eventually}} t(i, hi)) \\rightarrow \\bigcup_{i \\in S} s(i, hi) =^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 ‹_› :=
  (EventuallyLE.cardinal_bUnion hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.cardinal_bUnion hS fun i hi => (h i hi).symm.le)

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