Theorem: Matroid.girth_eq_top_iff (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
⊢ M.girth = ⊤ ↔ ∀ (C : Set α), M.Circuit C → C.Infinite
Tactic:
simp [girth, sInf_eq_top]
State after:
no goals