Theorem: FilterGame.Filter.mem_top_def (FilterGame/Solutions/Principal.lean)

State before:
α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
Tactic:
exact Iff.rfl
State after:
no goals