image2_subset_left

Mathlib.Data.Set.NAry

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

English

image2 is monotone in the left argument: if s1 ⊆ s2 then image2 f s1 t ⊆ image2 f s2 t.

Русский

image2 монотонна по левому аргументу: если s1 ⊆ s2, то image2 f s1 t ⊆ image2 f s2 t.

LaTeX

$$If s1 ⊆ s2, then image2 f s1 t ⊆ image2 f s2 t.$$

Lean4

theorem image2_subset_left (ht : t ⊆ t') : image2 f s t ⊆ image2 f s t' :=
  image2_subset Subset.rfl ht

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

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

Разделы

Аффилиация

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