image_insert_eq — Mathlib

English

The image of an insert of a into a set s is the insertion of f(a) into the image of s: f'' insert a s = insert (f a) (f'' s).

Русский

Образ вставки элемента a в множество s равен вставке f(a) в образ s: f'' insert a s = insert (f a) (f'' s).

LaTeX

$$$ f''\\operatorname{insert} a s = \\operatorname{insert}(f(a)) (f'' s). $$$

Lean4

theorem image_insert_eq {f : α → β} {a : α} {s : Set α} : f '' insert a s = insert (f a) (f '' s) := by grind

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