Theorem: Matroid.map_emptyOn (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ InjOn f (emptyOn α).E
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ (emptyOn α).map f ⋯ = emptyOn β
Tactic:
simp [← ground_eq_empty_iff]
State after:
no goals