image_subset_image₂_left

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.image_subset_image₂_left

English

If t ⊆ t', then image₂ f s t ⊆ image₂ f s t'.

Русский

Если T ⊆ T', то image₂ f S T ⊆ image₂ f S T'.

LaTeX

$$image₂_subset_right (hs : s ⊆ s') : image₂ f s t ⊆ image₂ f s' t$$

Lean4

theorem image_subset_image₂_left (hb : b ∈ t) : s.image (fun a => f a b) ⊆ image₂ f s t :=
  image_subset_iff.2 fun _ ha => mem_image₂_of_mem ha hb

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

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

Разделы

Аффилиация

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