eventuallyLE_iInter — Mathlib

English

If s is finite and for all i ∈ s we have s(i) ≤^l t(i), then the intersection over i ∈ s of s(i) is ≤^l the intersection over i ∈ s of t(i).

Русский

Если s конечное и для каждого i∈s выполняется s(i) ≤^l t(i), то пересечение ⋂_{i∈s} s(i) ≤^l ⋂_{i∈s} t(i).

LaTeX

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

Lean4

theorem _root_.Set.Finite.eventuallyLE_iInter {ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α}
    (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i) :=
  by
  have := hs.to_subtype
  rw [biInter_eq_iInter, biInter_eq_iInter]
  exact .iInter fun i ↦ hle i.1 i.2

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