exists_strictAnti — Mathlib

English

If α is a nonempty preorder with no minimal or maximal elements, there exists a strictly antitone function f: ℤ → α.

Русский

Если α — непустое частично упорядоченное множество без минимального и максимального элементов, существует строго антимонотонная функция f: ℤ → α.

LaTeX

$$$\\forall α\\,[Preorder α]\\,[Nonempty α]\\,[NoMinOrder α]\\,[NoMaxOrder α],\\ \\exists f:\\mathbb{Z} \\to α,\\ \\ StrictAnti f.$$$

Lean4

/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
antitone function `f : ℤ → α`. -/
theorem exists_strictAnti : ∃ f : ℤ → α, StrictAnti f :=
  exists_strictMono αᵒᵈ

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