iInter — Mathlib

English

Let l be a filter on α and ι a finite index set. If for every i, s(i) ≤^l t(i) (s_i is eventually contained in t_i along l), then the intersection over i of s(i) is eventually contained in the intersection over i of t(i).

Русский

Пусть l — фильтр на α и ι конечен. Если для каждого i выполняется s(i) ≤^l t(i), то ⋂_i s(i) ≤^l ⋂_i t(i).

LaTeX

$$$[\text{Finite } ι]\quad (\forall i, s(i) \le^l t(i)) \Rightarrow (\bigcap_i s(i) \le^l \bigcap_i t(i)).$$$

Lean4

protected theorem iInter [Finite ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) : (⋂ i, s i) ≤ᶠ[l] ⋂ i, t i :=
  (eventually_all.2 h).mono fun _x hx hx' ↦ mem_iInter.2 fun i ↦ hx i (mem_iInter.1 hx' i)

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