swap — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall a,b:\\alpha,\\; \\text{Trichotomous}(r)(a,b) \\Rightarrow \\text{Trichotomous}(swap\\,r)(a,b)$$$

Lean4

theorem swap (r) [IsTrichotomous α r] : IsTrichotomous α (swap r) :=
  ⟨fun a b => by simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b⟩

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