comp_subset_comp_left

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.comp_subset_comp_left

English

If R1 ⊆ R2, then R1 ○ S ⊆ R2 ○ S for any S.

Русский

Если R1 ⊆ R2, тогда R1 ○ S ⊆ R2 ○ S для любого S.

LaTeX

$$$(R_1 \subseteq R_2) \Rightarrow (R_1 \circ S) \subseteq (R_2 \circ S)$$$

Lean4

@[gcongr]
theorem comp_subset_comp_left {S : SetRel β γ} (hR : R₁ ⊆ R₂) : R₁ ○ S ⊆ R₂ ○ S :=
  comp_subset_comp hR .rfl

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

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

Разделы

Аффилиация

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