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

State before:
α : Type u_1
f g : Filter α
⊢ f ≤ g ↔ ∀ (s : Set α), s ∈ g → s ∈ f
Tactic:
exact Iff.rfl
State after:
no goals