strictAnti — Mathlib

English

If the domain α is a subsingleton, then every function f: α → β is strictly antitone.

Русский

Если область определения α состоит из одного элемента, любая функция f: α → β строго антимонотонна.

LaTeX

$$$\\text{Subsingleton}(\\alpha) \\Rightarrow \\forall f:\\alpha \\to \\beta,\\; \\mathrm{StrictAnti}(f)$$$

Lean4

protected theorem strictAnti [Subsingleton α] (f : α → β) : StrictAnti f := fun _ _ h ↦
  (h.ne <| Subsingleton.elim _ _).elim

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