Source indexedtheorem · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.EventuallyEq.finite_iInter

PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:311 to 323

Source documentation

The new Mathlib tool Finset.eventuallyEq_iInter will supersede this result.

Exact Lean statement

theorem EventuallyEq.finite_iInter {ι : Type*} {α : Type u_2} {l : Filter α} (s : Finset ι)
    {E : ι → Set α} {F : ι → Set α}
    (h : ∀ i ∈ s, E i =ᶠ[l] F i) :
    ⋂ i ∈ s, E i =ᶠ[l] ⋂ i ∈ s, F i

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem EventuallyEq.finite_iInter {ι : Type*} {α : Type u_2} {l : Filter α} (s : Finset ι)    {E : ι → Set α} {F : ι → Set α}    (h : ∀ i ∈ s, E i =ᶠ[l] F i) :    ⋂ i ∈ s, E i =ᶠ[l] ⋂ i ∈ s, F i := by  unfold Filter.EventuallyEq Filter.Eventually at h ⊢  simp only [eq_iff_iff] at h ⊢  rw [← Filter.biInter_finset_mem] at h  apply Filter.mem_of_superset h  intro a ha  change a ∈ ⋂ i ∈ s, E i ↔ a ∈ ⋂ i ∈ s, F i  simp only [mem_iInter, mem_setOf_eq] at ha ⊢  change ∀ i ∈ s, a ∈ E i ↔ a ∈ F i at ha  exact forall₂_congr ha