Theorems · Theorem · general topology

EventuallyLE.countable_iInter

Deprecated since 2026-03-03Use Filter.EventuallyLE.countable_iInter instead.

∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋂ i, s i ≤ᶠ[l] ⋂ i, t i

Alias of Filter.EventuallyLE.countable_iInter.

Defined in

Mathlib.Order.Filter.CountableInter

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableInterFilterCountable