comp_subset_comp_right

Mathlib.Data.Rel

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

English

If S1 ⊆ S2, then R ○ S1 ⊆ R ○ S2 for any R.

Русский

Если S1 ⊆ S2, тогда R ○ S1 ⊆ R ○ S2 для любого R.

LaTeX

$$(S_1 \subseteq S_2) \Rightarrow (R \circ S_1) \subseteq (R \circ S_2)$$

Lean4

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

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

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

Разделы

Аффилиация

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