image2_insert_right

Mathlib.Data.Set.NAry

URI: https://scilib.ai/kg/mathlib#Set.image2_insert_right

← MathLib Explorer

English

image2 f S (insert b T) = (f(·,b))'' S ∪ image2 f S T.

Русский

image2 f S (insert b T) = (f(·,b))'' S ∪ image2 f S T.

LaTeX

$$$$ \\operatorname{image2} f S (\\operatorname{insert} b T) = (\\lambda a. f(a,b))'' S \\cup \\operatorname{image2} f S T. $$$$

Lean4

@[simp]
theorem image2_insert_right : image2 f s (insert b t) = (fun a => f a b) '' s ∪ image2 f s t := by
  rw [insert_eq, image2_union_right, image2_singleton_right]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru