swap

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#IsTrans.swap

English

Swap preserves transitivity: if r is transitive on α, then swap(r) is transitive on α.

Русский

Swap сохраняет транзитивность: если r транзитивно на α, то swap(r) транзитивно на α.

LaTeX

$$$\forall r,\ [\text{IsTrans }\alpha\; r] \Rightarrow \text{IsTrans }\alpha\ (\mathrm{swap}\; r).$$$

Lean4

theorem swap (r) [IsTrans α r] : IsTrans α (swap r) :=
  ⟨fun _ _ _ h₁ h₂ => trans_of r h₂ h₁⟩

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

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

Разделы

Аффилиация

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