range_subset_insert_image_mulTSupport

English

The range of f is contained in the set {1} together with the image of f on the topological support: range f ⊆ insert 1 (f '' mulTSupport f).

Русский

Диапазон f содержится в {1} вместе с образом f на топологической опоре: range f ⊆ insert 1 (f '' mulTSupport f).

LaTeX

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

Lean4

@[to_additive]
theorem range_subset_insert_image_mulTSupport (f : X → α) : range f ⊆ insert 1 (f '' mulTSupport f) := by
  grw [← subset_mulTSupport f]; exact range_subset_insert_image_mulSupport f

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