English
If f maps s to t, then for any x, f maps insert x s to insert (f x) t.
Русский
Если f отображает s в t, то для любого элемента x отображение сохраняется после вставки x в s и f x в t.
LaTeX
$$$\\\\MapsTo f s t \\\\rightarrow \\\\forall x,\\\\MapsTo f (insert x s) (insert (f x) t)$$$
Lean4
theorem insert (h : MapsTo f s t) (x : α) : MapsTo f (insert x s) (insert (f x) t) := by
simpa [← singleton_union] using h.mono_right subset_union_right