image_subset_image2_left

Mathlib.Data.Set.NAry

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

English

If b ∈ t, then (f a b) image from s is contained in image2 f s t.

Русский

Если b ∈ t, то образ пары f a b от s содержится в image2 f s t.

LaTeX

$$$b \in t \implies (\{f a b : a ∈ s\}) ⊆ image2 f s t$$$

Lean4

theorem image_subset_image2_left (hb : b ∈ t) : (fun a => f a b) '' s ⊆ image2 f s t :=
  forall_mem_image.2 fun _ ha => mem_image2_of_mem ha hb

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

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

Разделы

Аффилиация

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