Theorem: FilterGame.Filter.as_basis_le_iff (FilterGame/Order.lean)

State before:
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b ↔ f ≤ Basis.as_filter b
Tactic:
sorry
State after:
no goals