Theorem: FilterGame.Basis.mem_def (FilterGame/Basis.lean)

State before:
α : Type u_1
b : Basis α
s : Set α
⊢ s ∈ b ↔ s ∈ b.sets
Tactic:
exact Iff.rfl
State after:
no goals