insert_image_compl_eq_range — Mathlib

English

For any f and x, inserting f(x) into the image of the complement of {x} yields the full range of f.

Русский

Для любой функции f и элемента x вставка f(x) в образ дополнения множества {x} дает полный диапазон функции.

LaTeX

$$$ \\mathrm{insert}(f(x), f''\\{x\\}^{c}) = \\mathrm{range}(f). $$$

Lean4

theorem insert_image_compl_eq_range (f : α → β) (x : α) : insert (f x) (f '' { x }ᶜ) = range f := by grind

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