Theorems · Theorem · general topology

Filter.exists_eventuallyEq_const_of_forall_separating

∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : α → β} [Nonempty β] (p : Set β → Prop)
  [HasCountableSeparatingOn β p Set.univ],
  (∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U) → ∃ a, f =ᶠ[l] Function.const α a

Defined in

Mathlib.Order.Filter.CountableSeparatingOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

CountableInterFilterNonemptyHasCountableSeparatingOn