cardinal_bInter — Mathlib

English

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

Русский

Если #ι < c и ∀ i, s_i =ᶠ[l] t_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_bInter {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_bInter hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.cardinal_bInter hS fun i hi => (h i hi).symm.le)

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