not_bddBelow_range_of_wellFoundedGT

English

Dual result: a StrictMono on a well-founded GT type yields the range not bounded below.

Русский

Двойной результат: StrictMono на хорошо упорядоченном GT типе даёт диапазон, не ограниченный снизу.

LaTeX

$$$\\text{StrictMono } f \\Rightarrow \\neg \\mathrm{BddBelow}(\\mathrm{Set.range}\\;f)$$$

Lean4

theorem not_bddBelow_range_of_wellFoundedGT {f : β → β} [WellFoundedGT β] [NoMinOrder β] (hf : StrictMono f) :
    ¬BddBelow (Set.range f) :=
  hf.dual.not_bddAbove_range_of_wellFoundedLT

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