RealFLub.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import AllCore Bool StdRing StdOrder RealLub.
(*---*) import RField RealOrder.
pragma +implicits.
(* lub for functions *)
op flub (F : 'a -> real) : real = lub (fun r => exists a, F a = r).
lemma flub_upper_bound r (F : 'a -> real) x :
(forall x, F x <= r) => F x <= flub F.
proof.
move => H. apply lub_upper_bound; 2: by exists x.
split; [by exists (F x) x|exists r => y [a] <-; exact H].
qed.
lemma flub_le_ub (F : 'a -> real) r :
(forall x, F x <= r) => flub F <= r.
proof.
move => H.
have ub_r : ub (fun (x : real) => exists (a : 'a), F a = x) r.
move => y [a] <-; exact H.
apply RealLub.lub_le_ub => //.
split; [by exists (F witness) witness| by exists r].
qed.