cardinal_iInter — Mathlib

English

If hic: #ι < c and h: ∀ i, s i =ᶠ[l] t i, then ⋂ i s i =ᶠ[l] ⋂ i t i.

Русский

Если #ι < c и s_i =ᶠ[l] t_i для каждого i, тогда ∩ s_i =ᶠ[l] ∩ t_i.

LaTeX

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

Lean4

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

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