swap — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall \\alpha\\;\\forall r:\\alpha \\to \\alpha \\to \\mathrm{Prop},\\; [\\text{IsPreorder } \\alpha \\; r] \\Rightarrow [\\text{IsPreorder } \\alpha \\; (swap\\,r)]$$$

Lean4

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

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