Сходящаяся последовательность к наименьшей верхней границе - PullRequest
Новая
       8

Сходящаяся последовательность к наименьшей верхней границе

0 голосов
/ 02 ноября 2018

Учитывая непустое подмножество действительных чисел E : R -> Prop, аксиома полноты дает наименьшую верхнюю границу l из E.

Есть ли конструктивная функция 

lub_approx_seq (E : R -> Prop) (l : R)
  : is_lub E l -> forall n:nat, { x:R | E x /\ l-1/n < x }

В классической математике мы утверждаем, что для всех n:nat, l-1/n не является верхней границей, поэтому существует x такой, что E x /\ l-1/n < x.

Но в конструктивной математике ~forall (не верхняя граница) слабее, чем exists.

Если для общего подмножества E это невозможно, существуют ли условия на E, которые делают это возможным?

EDIT

Меня особенно интересует случай, когда E - это бесконечно нисходящий интервал. Тогда сходящаяся последовательность - это просто fun n:nat => l-1/n, и осталось доказать следующее: 

Lemma lub_approx (E : R -> Prop) (l : R)
  : is_lub E l
    -> (forall x y : R, x < y -> E y -> E x) (* interval *)
    -> forall x : R, x < l -> E x
...