swap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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