Theorem: Matroid.unif_indep_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
I : Set (Fin b)
⊢ (unif a b).Indep I ↔ I.encard ≤ ↑a
Tactic:
rw [unif, unifOn_indep_iff, and_iff_left (subset_univ _)]
State after:
no goals