not_bddBelow_range_of_isSuccArchimedean

English

In the opposite direction, a StrictAnti function from NoMinOrder to SuccArchimedean codomain is not bounded above.

Русский

В противоположном направлении StrictAnti-функция из NoMinOrder в SuccArchimedean не ограничена сверху.

LaTeX

$$$ \text{If } f \text{ is StrictAnti, then } \mathrm{range}(f) \text{ is not BddAbove.}$$$

Lean4

theorem not_bddBelow_range_of_isSuccArchimedean [NoMinOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictAnti f) :
    ¬BddAbove (Set.range f) :=
  hf.dual_right.not_bddBelow_range_of_isPredArchimedean

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