clear X
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)