range_subset_singleton — Mathlib

English

The image of f is contained in {x} if and only if f is constant with value x.

Русский

Образ функции f содержится в множество {x} тогда и только тогда, когда f = константа x.

LaTeX

$$$$ \\operatorname{range}(f) \\subseteq \\{x\\} \\iff f = \\operatorname{const}_{\\iota} x $$$$

Lean4

theorem range_subset_singleton {f : ι → α} {x : α} : range f ⊆ { x } ↔ f = const ι x := by simp [funext_iff]

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