isTrans_iff_comp_subset_self

Mathlib.Data.Rel

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

English

A relation R is transitive if and only if R ∘ R ⊆ R.

Русский

Отношение R транзитивно тогда и только тогда, когда R ∘ R ⊆ R.

LaTeX

$$R.IsTrans ↔ (R ∘ R ⊆ R)$$

Lean4

theorem isTrans_iff_comp_subset_self : R.IsTrans ↔ R ○ R ⊆ R
    where
  mp _ := comp_subset_self
  mpr h := ⟨fun _ _ _ hx hy ↦ h ⟨_, hx, hy⟩⟩

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

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

Разделы

Аффилиация

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