α : Type u
β : Type v
γ : Type ?u.18901
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ univ ∈ f
α : Type u
β : Type v
γ : Type ?u.18901
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ range id ∈ f
rw [range_id]
no goals
α : Type u
β : Type v
γ : Type ?u.18901
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ univ ∈ f
exact univ_mem