exists_strictAnti' — Mathlib

English

There exists a strictly antitone function f: ℕ → α with f 0 = a, assuming NoMinOrder on α.

Русский

Существует строго антитонная функция f: ℕ → α с f(0) = a при условии NoMinOrder на α.

LaTeX

$$$[NoMinOrder α] (a : α) \\Rightarrow \\exists f : \\mathbb{N} \\to α, \\mathrm{StrictAnti} f \\land f 0 = a$$$

Lean4

/-- If `α` is a preorder with no maximal elements, then there exists a strictly antitone function
`ℕ → α` with any prescribed value of `f 0`. -/
theorem exists_strictAnti' [NoMinOrder α] (a : α) : ∃ f : ℕ → α, StrictAnti f ∧ f 0 = a :=
  exists_strictMono' (OrderDual.toDual a)

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