range_eq_image_mulTSupport_or — Mathlib

English

For any f, either the range equals the image of mulTSupport, or it equals that image with 1 added.

Русский

Для любого f диапазон либо равен образу mulTSupport, либо равен этому образу с добавлением 1.

LaTeX

$$$\operatorname{range}(f) = f(\operatorname{mulTSupport}(f)) \lor \operatorname{range}(f) = \operatorname{insert}(1, f(\operatorname{mulTSupport}(f)))$$$

Lean4

@[to_additive]
theorem range_eq_image_mulTSupport_or (f : X → α) :
    range f = f '' mulTSupport f ∨ range f = insert 1 (f '' mulTSupport f) :=
  (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _) (range_subset_insert_image_mulTSupport f)

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