cardinal_iInter — 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. Тогда ⋂ i s_i ≤ᶠ[l] ⋂ i t_i.

LaTeX

$$$#ι < c \\rightarrow (\\forall i, s_i \\le^l_{\\mathrm{Eventually}} t_i) \\rightarrow \\bigcap_i s_i \\le^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 :=
  ((eventually_cardinal_forall hic).2 h).mono fun _ hst hs => mem_iInter.2 fun i => hst _ (mem_iInter.1 hs i)

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