range_subset_insert_image_mulSupport

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

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