cardinal_iUnion — Mathlib

English

Let s, t : ι → Set α with hic: #ι < c and s i =ᶠ[l] t i for all i. Then ⋃ i, s i =ᶠ[l] ⋃ i, t i.

Русский

Пусть s_i =ᶠ[l] t_i для всех i; тогда объединение по i эквивалентно по отношению к l: ⋃ s_i =ᶠ[l] ⋃ t_i.

LaTeX

$$$#ι < c \\rightarrow (\\forall i, s_i =^l_{\\mathrm{Eventually}} t_i) \\rightarrow \\bigcup_i s_i =^l_{\\mathrm{Eventually}} \\bigcup_i t_i$$$

Lean4

theorem cardinal_iUnion {s t : ι → Set α} (hic : #ι < c) (h : ∀ i, s i =ᶠ[l] t i) : ⋃ i, s i =ᶠ[l] ⋃ i, t i :=
  (EventuallyLE.cardinal_iUnion hic fun i => (h i).le).antisymm
    (EventuallyLE.cardinal_iUnion hic fun i => (h i).symm.le)

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