swap — Mathlib

English

If a relation R on a set A is a strict total order, then the swapped relation on A is a strict total order.

Русский

Если отношение R на множестве A является строгим тотальным порядком, то переставленное отношение тоже строгий тотальный порядок.

LaTeX

$$$\\forall {\\alpha} (r) [IsStrictTotalOrder \\alpha \\; r], IsStrictTotalOrder \\alpha \\ (Function.swap \\ r)$$$

Lean4

theorem swap (r) [IsStrictTotalOrder α r] : IsStrictTotalOrder α (swap r) :=
  { IsTrichotomous.swap r, IsStrictOrder.swap r with }

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