range_eq_image_or_of_mulSupport_subset

English

If mulSupport f is contained in a set k, then the range of f is either equal to f''k or equal to insert 1 (f''k).

Русский

Если mulSupport f ⊆ k, то диапазон f либо равняется f''k, либо равняется вставке 1 в f''k.

LaTeX

$$$ \operatorname{range}(f) = f''k \ \lor\ \operatorname{range}(f) = \operatorname{insert} 1 \bigl(f''k\bigr) $$$

Lean4

@[to_additive]
theorem range_eq_image_or_of_mulSupport_subset {k : Set ι} (h : mulSupport f ⊆ k) :
    range f = f '' k ∨ range f = insert 1 (f '' k) :=
  by
  have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))
  grind

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