English
If s is nonempty, then the image of s under a constant function b is the singleton {b}.
Русский
Если множество s непусто, то образ под константной функцией b состоит из одного элемента: {b}.
LaTeX
$$$ s.Nonempty \\rightarrow (s.image (\\lambda x. b)) = \\{b\\} $$$
Lean4
theorem image_const {s : Finset α} (h : s.Nonempty) (b : β) : (s.image fun _ => b) = singleton b :=
mod_cast Set.Nonempty.image_const (coe_nonempty.2 h) b