simpa
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ ∀ (e : ↑I), M.Parallel' (↑e) (I.restrict φ e)
no goals