eventuallyLE_iInter — Mathlib

English

Let s be a finite set of indices. If for all i in s we have f(i) ≤^l g(i), then the intersection over i in s of f(i) is ≤^l the intersection over i in s of g(i).

Русский

Пусть s конечный набор индексов. Если для каждого i в s выполняется f(i) ≤^l g(i), тогда пересечение по i∈s f(i) ≤^l пересечение по i∈s g(i).

LaTeX

$$$[s \text{ finite}]\quad (\forall i \in s, f(i) \le^l g(i)) \Rightarrow (\bigcap_{i \in s} f(i) \le^l \bigcap_{i \in s} g(i)).$$$

Lean4

theorem _root_.Finset.eventuallyLE_iInter {ι : Type*} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) :
    (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i) :=
  .biInter s.finite_toSet hle

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