exists_strictAnti — Mathlib

English

If α is nonempty and NoMinOrder, there exists a strictly antitone function f: ℕ → α.

Русский

Если α непустое и нет минимального элемента, существует строго антитонная функция f: ℕ → α.

LaTeX

$$$[Nonempty α] [NoMinOrder α] : \\exists f : \\mathbb{N} \\to α, \\mathrm{StrictAnti} f$$$

Lean4

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

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