image_const — Mathlib

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

Похожие утверждения