Theorem: Set.surjOn_empty_iff (Matroid/ForMathlib/Function.lean)

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
⊢ SurjOn f ∅ t ↔ t = ∅
Tactic:
simp [SurjOn, subset_empty_iff]
State after:
no goals