no goals
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
m : MeasurableSpace α
f : α → β
⊢ ⊥ ∈ {a | ∀ᶠ (n : β) in map f (Measure.ae 0), n ≤ a}
simp [Set.mem_setOf_eq, EventuallyLE, ae_iff]