Module mathcomp.analysis.topology_theory.order_topology

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap all_classical.
From mathcomp Require Import topology_structure uniform_structure.
From mathcomp Require Import pseudometric_structure.

# Order topology ``` orderTopologicalType == a topology built from intervals order_topology T == the induced order topology on T ```

Import Order.TTheory GRing.Theory Num.Theory.

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

TODO: generalize this to a preOrder once that's available

HB.mixin Record Order_isNbhs d (T : Type) of Nbhs T & Order.Total d T := {

Note that just the intervals `]a, b doesn't work when the order has a top or bottom element, so we also need the rays `-oo, b and a, +oo *) itv_nbhsE : forall x : T, nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]) }. #[short(type="orderNbhsType")]
HB.structure Definition OrderNbhs d :=
  { T of Nbhs T & Order.Total d T & Order_isNbhs d T }.

#[short(type="orderTopologicalType")]
HB.structure Definition OrderTopological d :=
  { T of Topological T & Order.Total d T & Order_isNbhs d T }.

#[short(type="orderUniformType")]
HB.structure Definition OrderUniform d :=
  {T of Uniform T & OrderTopological d T}.

#[short(type="orderPseudoMetricType")]
HB.structure Definition OrderPseudoMetric d (R : numDomainType) :=
  {T of PseudoMetric R T & OrderTopological d T}.

Section order_topologies.
Local Open Scope order_scope.
Local Open Scope classical_set_scope.
Context {d} {T : orderTopologicalType d}.
Implicit Types x y : T.

Lemma rray_open x : open `]x, +oo[.

Proof.

rewrite openE /interior => z xoz; rewrite itv_nbhsE.
by exists `]x, +oo[%O => //; split => //; left.
Qed.

Hint Resolve rray_open : core.

Lemma lray_open x : open `]-oo, x[.

Proof.

rewrite openE /interior => z xoz; rewrite itv_nbhsE.
by exists (`]-oo, x[)%O => //; split => //; left.
Qed.

Hint Resolve lray_open : core.

Lemma itv_open x y : open `]x, y[.

Proof.

by rewrite set_itv_splitI /=; apply: openI. Qed.

Hint Resolve itv_open : core.

Lemma itv_open_ends_open (i : interval T) : itv_open_ends i -> open [set` i].

Proof.

case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]] []? => //.
by rewrite set_itvE; exact: openT.
Qed.

Lemma rray_closed x : closed `[x, +oo[.

Proof.

by rewrite -setCitvl closedC. Qed.

Hint Resolve rray_closed : core.

Lemma lray_closed x : closed `]-oo, x].

Proof.

by rewrite -setCitvr closedC. Qed.

Hint Resolve lray_closed : core.

Lemma itv_closed x y : closed `[x, y].

Proof.

by rewrite set_itv_splitI; apply: closedI => /=. Qed.

Hint Resolve itv_closed : core.

Lemma itv_closure x y : closure `]x, y[ `<=` `[x, y].

Proof.

rewrite closureE => r; apply; split => //.
by apply: subset_itvScc => /=; rewrite bnd_simp.
Qed.

Lemma itv_closed_infimums (A : set T) : A !=set0 -> closed A ->
infimums A `<=` A.

Proof.

move=> [a0 Aa0] + l [loL] hiL; rewrite closure_id => -> => U.
rewrite itv_nbhsE => -[[p q []]].
have [E|E] := eqVneq ([set` Interval (BSide true l) q] `&` A) set0; last first.
  case/set0P: E => a [lqa ?] ? lpq pqU; exists a; split => //.
  apply: pqU; move: lpq lqa; rewrite /= ?inE => lpq /le_trans; apply.
  by move: lpq => /andP [? ?]; exact/andP.
case: q E.
- move=> b q /[swap] /itv_open_ends_rside -> E lpq ; suff : lbound A q.
    move/hiL => + _; rewrite leNgt; apply: contraNP => _.
    by move: lpq; rewrite in_itv => /andP [].
  move=> a Aa; have : (~` (`[l, q[ `&` A)) a by rewrite E.
  rewrite setCI => -[|//]; rewrite setCitv /= ?in_itv/= ?andbT => -[|//].
  by rewrite ltNge (loL _ Aa).
- move=> b _ /itv_open_ends_rinfty -> lpo poU; exists a0; split => //.
  apply: poU; move: lpo; rewrite /= ?itv_boundlr /= => /andP[pl _]; apply/andP.
  by split => //; exact/(le_trans pl)/loL.
Qed.

Lemma itv_closed_supremums (A : set T) : A !=set0 -> closed A ->
supremums A `<=` A.

Proof.

move=> [a0 Aa0] + l [upL] lbL; rewrite closure_id => -> => U.
rewrite itv_nbhsE => -[[p q[]]].
have [E|E] := eqVneq ([set` Interval p (BSide false l)] `&` A) set0; last first.
  case/set0P: E => a [lqa ?] ? lpq pqU; exists a; split => //.
  apply: pqU; move: lpq lqa; rewrite /= ?inE => lpq /le_trans; apply.
  by move: lpq => /andP [? ?]; exact/andP.
case: p E.
- move=> b p /[swap] /itv_open_ends_lside -> E lpq ; suff : ubound A p.
    move/lbL => + _; rewrite leNgt; apply: contraNP => _.
    by move: lpq; rewrite in_itv => /andP [].
  move=> a Aa; have : (~` (`]p, l] `&` A)) a by rewrite E.
  rewrite setCI => -[|//]; rewrite setCitv /= ?in_itv/= ?andbT => -[//|].
  by rewrite ltNge (upL _ Aa).
- move=> b _ /itv_open_ends_linfty -> lpo poU; exists a0; split => //.
  apply: poU; move: lpo; rewrite /= ?itv_boundrl /= => /andP[_ pl]; apply/andP.
  by split => //; exact/(le_trans _ pl)/upL.
Qed.

Let sub_open_mem x (U : set T) (i : interval T) :=
[/\ [set` i] `<=` U, open [set` i] & x \in i].

Lemma clopen_bigcup_clopen x (U : set T) : clopen U -> U x ->
clopen (\bigcup_(i in sub_open_mem x U) [set` i]).

Proof.

pose I := \bigcup_(i in sub_open_mem x U) [set` i].
move=> clU Ux; split; first by apply: bigcup_open => ? [].
have cIV : closure I `<=` U.
  rewrite closureE => z /(_ U); apply; split; first by case: clU.
  by move=> ? [? [+ _ _]]; exact.
apply/closure_id; rewrite eqEsubset; split; first exact: subset_closure.
move=> z cIi; have Uz : U z by exact: cIV.
case: clU => + _; rewrite {1}openE => /(_ _ Uz).
rewrite /interior /= itv_nbhsE /= => -[i [/itv_open_ends_open oi iy] siU].
case/(_ [set` i]): cIi; first by move: oi; rewrite openE; exact.
move=> /= w [[j [jU oJ jy jw]]] wi; exists (i `|` j)%O; first last.
  exact/(le_trans iy)/leUl.
split; first by rewrite itv_setU ?{1}subUset //; exists w.
by rewrite itv_setU ?{1}subUset //; [exact: openU | exists w].
exact/(le_trans jy)/leUr.
Qed.

End order_topologies.
Hint Resolve lray_open : core.
Hint Resolve rray_open : core.
Hint Resolve itv_open : core.
Hint Resolve lray_closed : core.
Hint Resolve rray_closed : core.
Hint Resolve itv_closed : core.

Definition order_topology (T : Type) : Type := T.

Section induced_order_topology.

Context {d} {T : orderType d}.

Local Notation oT := (order_topology T).

HB.instance Definition _ := isPointed.Build (interval T) (`]-oo,+oo[).

HB.instance Definition _ := Order.Total.on oT.
HB.instance Definition _ := @isSubBaseTopological.Build oT
  (interval T) (itv_is_ray) (fun i => [set` i]).

Lemma order_nbhs_itv (x : oT) : nbhs x = filter_from
    (fun i => itv_open_ends i /\ x \in i)
    (fun i => [set` i]).

Proof.

rewrite eqEsubset; split => U; first last.
  case=> /= i [ro xi /filterS]; apply; move: ro => [rayi|].
    exists [set` i]; split => //=.
    exists [set [set` i]]; last by rewrite bigcup_set1.
    move=> A ->; exists (fset1 i); last by rewrite set_fset1 bigcap_set1.
    by move=> ?; rewrite !inE => /eqP ->.
  case: i xi => [][[]l|[]] [[]r|[]] xlr []//=; exists `]l, r[%classic.
  split => //; exists [set `]l, r[%classic]; last by rewrite bigcup_set1.
  move=> ? ->; exists [fset `]-oo, r[ ; `]l, +oo[]%fset.
    by move=> ?; rewrite !inE => /orP[] /eqP ->.
  rewrite set_fsetU !set_fset1 bigcap_setU !bigcap_set1.
  by rewrite (@set_itv_splitI _ _ `]l, r[) /= setIC.
case=> ? [[ I Irp] <-] [?] /[dup] /(Irp _) [F rayF <-] IF Fix IU.
pose j := \big[Order.meet/`]-oo, +oo[]_(i <- F) i.
exists j; first split.
- rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//.
  + apply: big_ind; [by left| exact: itv_open_endsI|].
    by move=> i /rayF /set_mem ?; left.
  + by move=> p /=; rewrite !inE/=; exact: andb_id2l.
- pose f (i : interval T) : Prop := x \in i; suff : f j by [].
  rewrite /j (@eq_fbig_cond _ _ _ _ _ F _ (mem F) _ id)//=.
  + by apply: big_ind => //=; rewrite /f /= => a ? xa ?; rewrite in_itvI xa.
  + by move=> p /=; rewrite !inE/=; exact: andb_id2l.
- suff -> : [set` j] = \bigcap_(i in [set` F]) [set` i].
    by move=> i Fi; apply: IU; exists (\bigcap_(i in [set` F]) [set` i]).
  rewrite -bigsetI_fset_set ?set_fsetK//.
  pose f (i : interval T) (j : set T) : Prop := [set` i] = j.
  suff : f j (\big[setI/[set: T]]_(i <- F) [set` i]) by [].
  rewrite /j big_mkcond /=; apply: big_ind2; rewrite /f ?set_itvE//.
  by move=> ? ? ? ? <- <-; rewrite itv_setI.
Qed.

HB.instance Definition _ := Order_isNbhs.Build _ oT order_nbhs_itv.
End induced_order_topology.
]

Files

Module mathcomp.analysis.topology_theory.order_topology