Theorems · Theorem · general topology

eventually_countable_forall

∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {p : α → ι → Prop},
  (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Defined in

Mathlib.Order.Filter.CountableInter

Cited by

7 results in Mathlib

Foundations

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

Assumes

CountableInterFilterCountable