apply_eq_of_range_eq_singleton — Mathlib

English

If the range of f is a singleton {b}, then f maps every a ∈ domain to b; i.e., f a = b for all a.

Русский

Если диапазон f равен одиночке {b}, тогда для любого a выполняется f a = b.

LaTeX

$$$ \\operatorname{range} f = \\{ b \\} \\Rightarrow \\forall a, f a = b. $$$

Lean4

theorem apply_eq_of_range_eq_singleton {f : α → β} {b : β} (h : range f = { b }) (a : α) : f a = b := by
  simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a

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