image_subset_image2_right

Mathlib.Data.Set.NAry

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

English

If a ∈ s, then f a '' t ⊆ image2 f s t.

Русский

Если a ∈ s, то изображение f a '' t ⊆ image2 f s t.

LaTeX

$$If a ∈ s, then f a '' t ⊆ image2 f s t.$$

Lean4

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

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

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

Разделы

Аффилиация

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