Theorems · Theorem · general topology

Filter.EventuallyLE.countable_iUnion

∀ {ι : 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

Defined in

Mathlib.Order.Filter.CountableInter

Cited by

3 results in Mathlib

Foundations

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

Assumes

CountableInterFilterCountable