Commit 2022-04-07 18:41 44c31d8f

feat(data/finset/basic): add map_injective and sigma_equiv_option_of_inhabited (#13083) Adds map_injective (f : α ↪ β) : injective (map f) := (map_embedding f).injective and sigma_equiv_option_of_inhabited [inhabited α] : Σ (β : Type u), α ≃ option β. Extracted from @huynhtrankhanh's https://github.com/leanprover-community/mathlib/pull/11162, moved here to a separate PR