Mapping_is_Constant_iff_Image_is_Singleton
Provedconstant-mappingsproofwikisingletons
A mapping is a constant mapping if and only if its image is a singleton.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Image
Formal statement
theorem Mapping_is_Constant_iff_Image_is_Singleton {α β : Type _} [Nonempty α] (f : α → β) : (∃ c, ∀ x, f x = c) ↔ (∃ c, Set.range f = {c}) := by sorrySource