English
For any f: ι → M, the range of f is contained in {1} together with the image of mulSupport f, i.e., every value of f is either 1 or comes from some i where f(i) ≠ 1.
Русский
Для любой f: ι → M множество значений f лежит внутри {1} вместе с образами mulSupport f, то есть каждое значение f либо равно 1, либо получено на некотором i, где f(i) ≠ 1.
LaTeX
$$$ \operatorname{range}(f) \subseteq \{1\} \cup \bigl( f''\operatorname{mulSupport}(f) \bigr) $$$
Lean4
@[to_additive]
theorem range_subset_insert_image_mulSupport (f : ι → M) : range f ⊆ insert 1 (f '' mulSupport f) := by
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using fun x (hx : x ∈ mulSupport f) ↦
mem_image_of_mem f hx