Theorem: Matroid.truncateTo_top (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo ⊤).E, (M.truncateTo ⊤).Indep I ↔ M.Indep I
Tactic:
simp [truncateTo]
State after:
no goals