Theorems · Theorem · general topology

Filter.eventually_all_finset

∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
  (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Defined in

Mathlib.Order.Filter.Finite

Cited by

12 results in Mathlib

Foundations

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