image2_inter_subset_right

Mathlib.Data.Set.NAry

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

English

image2 f S (T ∩ T') ⊆ image2 f S T ∩ image2 f S T'.

Русский

image2 f S (T ∩ T') ⊆ image2 f S T ∩ image2 f S T'.

LaTeX

$$$$ \\operatorname{image2} f S (T \\cap T') \\subseteq \\ operatorname{image2} f S T \\cap \\ operatorname{image2} f S T'. $$$$

Lean4

theorem image2_inter_subset_right : image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t' :=
  Monotone.map_inf_le (fun _ _ ↦ image2_subset_left) t t'

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

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

Разделы

Аффилиация

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