Theorem: FilterGame.Filter.mem_as_basis_def (FilterGame/Basis.lean)

State before:
α : Type u_1
f : Filter α
t : Set α
⊢ t ∈ as_basis f ↔ t ∈ f
Tactic:
exact Iff.rfl
State after:
no goals