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

State before:
α : Type u_1
b c : Basis α
⊢ b ≤' c ↔ ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact Iff.rfl
State after:
no goals