left_subset_comp

Mathlib.Data.Rel

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

English

R ⊆ R ○ S whenever S is reflexive.

Русский

R ⊆ R ○ S при условии, что S рефлексивно.

LaTeX

$$R ⊆ R.\mathrm{comp} S$$

Lean4

theorem left_subset_comp {R : SetRel α β} [S.IsRefl] : R ⊆ R ○ S := by simpa using comp_subset_comp_right id_subset

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

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

Разделы

Аффилиация

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