symm — Mathlib

English

If s is a chain for r, then it is a chain for the flipped relation.

Русский

Если s — цепь относительно r, то она цепь относительно перевёрнутого отношения.

LaTeX

$$$\operatorname{IsChain}(r,s) \to \operatorname{IsChain}(\mathrm{flip}(r), s)$$$

Lean4

/-- This can be used to turn `IsChain (≥)` into `IsChain (≤)` and vice-versa. -/
theorem symm (h : IsChain r s) : IsChain (flip r) s :=
  h.mono' fun _ _ => Or.symm

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