image2_insert_left

Mathlib.Data.Set.NAry

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

← MathLib Explorer

English

image2 f (insert a S) T = image (f(a,·)) T ∪ image2 f S T.

Русский

image2 f (insert a S) T = image (f(a,·)) T ∪ image2 f S T.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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