no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' ↑∅)
simp [InjOn]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ ↑(preimage ∅ f (_ : ∀ (a : α), a ∈ f ⁻¹' ↑∅ → ∀ (a_2 : α), a_2 ∈ f ⁻¹' ↑∅ → f a = f a_2 → a = a_2)) = ↑∅
simp