image2_mem_map₂

Mathlib.Order.Filter.NAry

URI: https://scilib.ai/kg/mathlib#Filter.image2_mem_map₂

English

If f1 ≤ f2 and g1 ≤ g2, then map₂ m f1 g1 ≤ map₂ m f2 g2.

Русский

Если f1 ≤ f2 и g1 ≤ g2, то map₂ m f1 g1 ≤ map₂ m f2 g2.

LaTeX

$$$f_1 \\leq f_2 \\land g_1 \\leq g_2 \\Rightarrow \\mathrm{map\\_2}\\; m\\; f_1\\; g_1 \\leq \\mathrm{map\\_2}\\; m\\; f_2\\; g_2$$$

Lean4

theorem image2_mem_map₂ (hs : s ∈ f) (ht : t ∈ g) : image2 m s t ∈ map₂ m f g :=
  ⟨_, hs, _, ht, Subset.rfl⟩

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

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

Разделы

Аффилиация

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