cardinal_bInter — Mathlib

English

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

Русский

Пусть S ⊆ ι, #S < c, и для каждого i ∈ S, h_i, 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 \\le^l_{\\mathrm{Eventually}} t_i hi) \\rightarrow \\bigcap_{i \\in S} s_i hi \\le^l_{\\mathrm{Eventually}} \\bigcap_{i \\in S} t_i hi$$$

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 ‹_› :=
  by
  simp only [biInter_eq_iInter]
  exact EventuallyLE.cardinal_iInter hS fun i => h i i.2

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