swap — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall {\\alpha} \\; (r) [IsStrictOrder \\alpha \\; r] \\\\: IsStrictOrder \\alpha \\ (Function.swap \\ r)$$$

Lean4

theorem swap (r) [IsStrictOrder α r] : IsStrictOrder α (swap r) :=
  { @IsIrrefl.swap α r _, @IsTrans.swap α r _ with }

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