analysis/classical/sup.v at 30a83f0db7ff9de4e4c3ec417f350fa652bbfd7e · math-comp/analysis · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory.
Local Open Scope order_scope.

About family.

From mathcomp Require Import classical_sets boolp.

Record universe := Universe {universe_sort :> Type; El : universe_sort -> Type}.
(* Definition universe_universe := @Universe universe universe_sort. *)

Definition family (U : universe) X := {I : U & {P : set (El I) & El I -> X}}.

Definition finfamily := @family (@Universe finType (id : finType -> Type)).
Definition seqfamily := @family (@Universe {A : eqType & seq A} (fun X => {x | x \in projT2 X})).
(* Definition seqfamily_ (I : eqType) := @family (seq I) (fun s => {x | x \in s}). *)

HB.mixin Record isSup d (T : porderType d) (pT : predType T)
    (Q : set pT) (sup : pT -> T) := {
  supP : forall (A : Q) (y : T),
    reflect (forall x : T, x \in val A -> x <= y) (sup (val A) <= y)
}.
HB.structure Definition Sup d T pT Q := {sup of @isSup d T pT Q sup}.

(* HB.mixin Record isSupFam d (I : porderType d) T Q (sup : set I -> (I -> T) -> T) := { *)
(*   supP : F (y : T), *)
(*     reflect (forall x : T, x \in val A -> x <= y) (sup (val A) <= y) *)
(* }. *)
(* HB.structure Definition Sup d T pT Q := {sup of @isSup d T pT Q sup}. *)


HB.mixin Record isLeftAdjoint d d' (C : porderType d') (D : porderType d)
    (R : D -> C) (L : C -> D) := {
  LeftP : forall A y, (L A <= y) = (A <= R y)
}.
HB.structure Definition LeftAdjoint d d' T U R :=
  {L of @isLeftAdjoint d d' T U R L}.

From mathcomp Require Import classical_sets boolp reals constructive_ereal ereal.
Local Open Scope classical_set_scope.
Section RealSup.
Variable (R : realType).

Lemma sup_isSup : @isSup _ R (set R) (@has_ubound _ R `&` nonempty) sup.
Proof.
split=> -[/= A /[!inE]/= -[Abnd AN0]] y; apply: (iffP idP).
  move=> supA_le_y x xA; rewrite (le_trans _ supA_le_y)//.
  by apply/ub_le_sup => //=; exact/set_mem.
by move=> ble; apply/ge_sup => // x /mem_set; apply/ble.
Qed.
HB.instance Definition _ := sup_isSup.

Lemma ereal_sup_isSup :
  @isSup _ (\bar R) (set (\bar R)) [set: set (\bar R)] (@ereal_sup R).
Proof.
split=> -[/= A _] y; apply: (equivP ereal_supP).
by split=> [Ay x /set_mem|Ay x /mem_set]; apply: Ay.
Qed.
HB.instance Definition _ := ereal_sup_isSup.