seq_eq_image2

Mathlib.Data.Set.Operations

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

English

seq s t equals image2 of the map f a ↦ f(a) on s and t.

Русский

seq s t равно image2 от отображения f(a) = f(a) на s и t.

LaTeX

$$$$ \\text{seq}(s,t) = \\operatorname{image2}(\\lambda f\\, a \\mapsto f(a))\\, s\\, t $$$$

Lean4

theorem seq_eq_image2 (s : Set (α → β)) (t : Set α) : seq s t = image2 (fun f a ↦ f a) s t :=
  rfl

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

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

Разделы

Аффилиация

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