isTrans_symmetrize

Mathlib.Data.Rel

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

English

If R is transitive, then its symmetrize is transitive.

Русский

Если R транзитивно, то его симметризованное сохраняет транзитивность.

LaTeX

$$$\forall {R : \text{SetRel } \alpha \alpha}, [R.IsTrans] \Rightarrow R.\text{symmetrize}.IsTrans$$

Lean4

instance isTrans_symmetrize [R.IsTrans] : R.symmetrize.IsTrans where
  trans _a _b _c hab hbc := ⟨R.trans hab.1 hbc.1, R.trans hbc.2 hab.2⟩

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

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

Разделы

Аффилиация

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