Module mathcomp.analysis.topology_theory.subspace_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import topology_structure uniform_structure compact.
From mathcomp Require Import pseudometric_structure connected initial_topology.
From mathcomp Require Import product_topology.

# Subspaces of topological spaces ``` subspace A == for (A : set T), this is a copy of T with a topology that ignores points outside A incl_subspace x == with x of type subspace A with (A : set T), inclusion of subspace A into T nbhs_subspace x == filter associated with x : subspace A from_subspace A f == function of type `subspace A -> U` given a function f of type `A -> U` The purpose of this definition is to preserve the pretty-printing of the notation {within _, continuous _} below. Its use is however likely to be later superseded by a better (compositional) mechanism. {within A, continuous f} := continuous (from_subspace A f)) subspace_ent A == subspace entourages subspace_ball A == balls of the pseudometric subspace structure continuousSubspaceType A B == type of continuous functions from set A to set B with domain subspace A The HB structure is ContinuousFun. ``` `subdiagonal X` : `:= [set z | (A z.1 /\ A z.2) \/ z.1 = z.2]`

Reserved Notation "{ 'within' A , 'continuous' f }"
  (format "{ 'within' A , 'continuous' f }").

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition { : Type} ( : set T) := T.
Arguments subspace {T} _ : simpl never.

Definition { } ( : subspace A) : T := x.

Section Subspace.
Context { : topologicalType} ( : set T).
Definition ( : subspace A) : set_system (subspace A) :=
  if x \in A then within A (nbhs x) else globally [set x].

Variant : Prop -> Prop -> bool -> set_system T -> Type :=
  | :
      A x -> nbhs_subspace_spec x True False true (within A (nbhs x))
  | :
    ~ A x -> nbhs_subspace_spec x False True false (globally [set x]).

Lemma :
  nbhs_subspace_spec x (A x) (~ A x) (x \in A) (nbhs_subspace x).

Proof.

rewrite /nbhs_subspace; case:(boolP (x \in A)); rewrite ?(inE, notin_setE) => xA.
by rewrite (@propext (A x) True)// not_True; constructor.
by rewrite (@propext (A x) False)// not_False; constructor.
Qed.

Lemma ( : T) : A x -> within A (nbhs x) = nbhs_subspace x.

Proof.

by case: nbhs_subspaceP_subproof. Qed.

Lemma ( : T) : ~ A x -> globally [set x] = nbhs_subspace x.

Proof.

by case: nbhs_subspaceP_subproof. Qed.

Lemma ( : subspace A) : ProperFilter (nbhs_subspace x).

Proof.

case: nbhs_subspaceP_subproof => ?; last exact: globally_properfilter.
by apply: within_nbhs_proper; apply: subset_closure.
Qed.

..copy (subspace A) _.

..Build (subspace A) nbhs_subspace.

Lemma ( : subspace A) :
nbhs_subspace_spec x (A x) (~ A x) (x \in A) (nbhs x).

Proof.

exact: nbhs_subspaceP_subproof. Qed.

Lemma ( : subspace A) : nbhs p B -> B p.

Proof.

by case: nbhs_subspaceP => ? => [/nbhs_singleton|]; apply. Qed.

Lemma ( : subspace A) : nbhs p B -> nbhs p (nbhs^~ B).

Proof.

case: nbhs_subspaceP => [|] Ap.
by move=> /nbhs_interior; apply: filterS => y A0y Ay; case: nbhs_subspaceP.
by move=> E x ->; case: nbhs_subspaceP.
Qed.

..Build (subspace A)
nbhs_subspace_filter nbhs_subspace_singleton nbhs_subspace_nbhs.

Lemma ( : set_system T) ( : T) : Filter F -> A x ->
(F --> (x : subspace A)) <-> (F --> within A (nbhs x)).

Proof.

by case: _ / nbhs_subspaceP. Qed.

Lemma { : topologicalType} ( : T -> S) :
continuous (f : subspace A -> S) <->
(forall , A x -> f @ within A (nbhs x) --> f x) .

Proof.

split => [ctsf x Ax W /=|wA x].
by rewrite nbhs_simpl //= nbhs_subspace_in //=; apply: ctsf.
rewrite /continuous_at; case: _ / (nbhs_subspaceP x) => Ax.
exact: (cvg_trans _ (wA _ Ax)).
by move=> ? /nbhs_singleton //= ?; rewrite nbhs_simpl => ? ->.
Qed.

Lemma { : topologicalType} ( : subspace A -> S) :
{in A, f =1 g} -> continuous f -> continuous g.

Proof.

rewrite ?subspace_continuousP => feq L x Ax; rewrite -(feq x) ?inE //.
by apply: cvg_trans _ (L x Ax); apply: fmap_within_eq=> ? ?; rewrite feq.
Qed.

Lemma { : topologicalType} ( : subspace A -> U) :
continuous f = {in A, continuous f}.

Proof.

rewrite propeqE in_setP subspace_continuousP /continuous_at //=; split.
by move=> Q x Ax; case: (nbhs_subspaceP x) => //=; exact: Q.
by move=> + x Ax => /(_ x Ax); case: (nbhs_subspaceP x) => //=; exact: Q.
Qed.

Lemma ( : T) :
A° x -> nbhs x = (nbhs (x : subspace A)).

Proof.

move=> /[dup] /[dup] /interior_subset ? /within_interior <- ?.
by case: RHS / nbhs_subspaceP.
Qed.

Lemma ( : set T) ( : T) : A x ->
nbhs (x : subspace A) U <->
exists2 , nbhs (x : T) V & U `&` A = V `&` A.

Proof.

by case: (nbhs _) / nbhs_subspaceP; rewrite // ?withinE. Qed.

Lemma : continuous incl_subspace.

Proof.

by apply/subspace_continuousP => x Ax; apply: cvg_within. Qed.

Section SubspaceOpen.

Lemma ( : subspace A) : ~ A x -> open [set x].

Proof.

move=> /nbhs_subspace_out E; have : nbhs x [set x] by rewrite /nbhs //= -E.
rewrite nbhsE => [[U []]] oU Ux Usub; suff : U = [set x] by move=> <-.
by rewrite eqEsubset; split => // t ->.
Qed.

Lemma ( : set (subspace A)) : U `<=` ~` A -> open U.

Proof.

move=> Usub; rewrite -(image_id U) -bigcup_imset1.
by apply: bigcup_open => ? ?; apply: open_subspace1out; exact: Usub.
Qed.

Lemma : open (A : set (subspace A)).

Proof.

by move=> ?; case: nbhs_subspaceP => //= ? ?; apply: withinT. Qed.

Lemma ( : set (subspace A)) : open (U `&` A) = open U.

Proof.

apply/propext; split; last first.
by move=> oU; apply: openI => //; apply: open_subspaceT.
move=> oUA; rewrite (_ : U = (U `&` A) `|` (U `&` ~`A)).
by rewrite -setIUr setUCr setIT.
by apply: openU => //; apply: open_subspace_out => ? [].
Qed.

Lemma ( : set (subspace A)) :
open (A `&` U : set (subspace A)) = open U.

Proof.

by rewrite setIC open_subspaceIT. Qed.

Lemma : closed (A : set (subspace A)).

Proof.

rewrite -(setCK A);
by apply: open_closedC; rewrite -open_subspaceIT setICl; exact: open0.
Qed.

Lemma ( : set T) :
open (U : set (subspace A)) <->
exists2 , open (V : set T) & V `&` A = U `&` A.

Proof.

split; first last.
  case=> V oV UV; rewrite -open_subspaceIT -UV.
  move=> x //= []; case: nbhs_subspaceP; rewrite //= withinE.
  move=> Ax Vx _; exists V; last by rewrite -setIA setIid.
  by move: oV; rewrite openE /interior; exact.
rewrite -open_subspaceIT => oUA.
have oxF ( : T) : (U `&` A) x ->
    exists2 , open_nbhs (x : T) V & V `&` A `<=` U `&` A.
  move=> /[dup] UAx /= [Ux Ax].
  have := oUA _ UAx; case: nbhs_subspaceP => // _.
  rewrite withinE /= => -[V nbhsV]; rewrite -setIA setIid => UV.
  exists V°; first rewrite open_nbhsE; first split => //.
  - exact: open_interior.
  - exact: nbhs_interior.
  - by rewrite UV => t [/interior_subset].
pose f ( : T) :=
  if pselect ((U `&` A) x) is left e then projT1 (cid2 (oxF x e)) else set0.
set V := \bigcup_( in U `&` A) f x; exists V.
  apply: bigcup_open => i UAi; rewrite /f; case: pselect => // ?; case: cid2.
  by move=> //= W; rewrite open_nbhsE => -[].
rewrite eqEsubset /V /f; split.
  move=> t [[u]] UAu /=; case: pselect => //= ?.
  by case: cid2 => //= W _ + ? ? ; apply; exact.
move=> t UAt; split => //; last by case: UAt.
exists t => //; case: pselect => //= [[? ?]].
by case: cid2 => //= W [].
Qed.

Lemma ( : set T) :
closed (U : set (subspace A)) <->
exists2 , closed (V : set T) & V `&` A = U `&` A.

Proof.

rewrite -openC open_subspaceP !exists2E.
under [X in _ <-> X]eq_exists => x do rewrite -openC.
by split => -[V [? VU]]; exists (~` V); rewrite ?setCK //;
move/(congr1 setC): VU; rewrite ?eqEsubset ?setCI ?setCK; firstorder.
Qed.

Lemma ( : set T) :
open (U : set T) -> open (U : set (subspace A)).

Proof.

by move=> oU; apply/open_subspaceP; exists U. Qed.

Lemma ( : set T) :
closed (U : set T) -> closed (U : set (subspace A)).

Proof.

by move=> /closed_openC/open_subspaceW/open_closedC; rewrite setCK. Qed.

Lemma ( : set (subspace A)) : open A ->
open (U `&` A : set T) = open U.

Proof.

move=> oA; apply/propext; rewrite open_subspaceP.
split=> [|[V oV <-]]; last exact: openI.
by move=> oUA; exists (U `&` A); rewrite // -setIA setIid.
Qed.

Lemma ( : set (subspace A)) : open A -> open (A `&` U) = open U.

Proof.

by move=> oA; rewrite -setIC open_setIS. Qed.

Lemma ( : set (subspace A)) : closed A ->
closed (U `&` A : set T) = closed U.

Proof.

move=> oA; apply/propext; rewrite closed_subspaceP.
split=> [|[V oV <-]]; last exact: closedI.
by move=> oUA; exists (U `&` A); rewrite // -setIA setIid.
Qed.

Lemma ( : set (subspace A)) :
closed A -> closed (A `&` U) = closed U.

Proof.

by move=> oA; rewrite -setIC closed_setIS. Qed.

Lemma ( : set T) :
U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A.

Proof.

have /closed_subspaceP := @closed_closure _ (U : set (subspace A)).
move=> [V clV VAclUA] /[dup] /(@closureS (subspace _)).
have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC.
move=> UsubA; rewrite eqEsubset; split.
  apply: setSI; rewrite closureE.
  apply: smallest_sub (@subset_closure _ U).
  by apply: closed_subspaceW; exact: closed_closure.
rewrite -VAclUA; apply: setSI; rewrite closureE //=.
apply: smallest_sub => //; apply: subset_trans (@subIsetl _ V A).
rewrite VAclUA subsetI; split => //.
exact: (@subset_closure _ (U : set (subspace A))).
Qed.

End SubspaceOpen.

Lemma ( : set T) :
compact (U `&` A : set (subspace A)) <-> compact (U `&` A : set T).

Proof.

rewrite ?compact_ultra /=.
split=> + F UF FUA => /(_ F UF FUA) [x] [[Ux Ax] Fp].
  exists x; split=> //; move/subspace_cvgP: Fp => /(_ Ax) Fx.
  by apply: cvg_trans; [exact: Fx | exact: cvg_within].
exists x; split=> //; apply/subspace_cvgP => //.
rewrite withinE => W/= -[V nbhsV WV]; apply: filterS (V `&` (U `&` A)) _ _ _.
  by rewrite setIC -setIA [A `&` _]setIC -WV=>?[]?[].
by apply: filterI; rewrite nbhs_simpl //; exact: Fp.
Qed.

Lemma : connected A <->
(forall , @clopen (subspace A) U ->
U `<=` A -> U !=set0 -> U = A).

Proof.

split.
  move=> + U [/open_subspaceP oU /closed_subspaceP cU] UA U0; apply => //.
  - case: oU => V oV VAUA; exists V; rewrite // setIC VAUA.
    exact/esym/setIidPl.
  - case: cU => V cV VAUA; exists V; rewrite // setIC VAUA.
    exact/esym/setIidPl.
move=> clpnA U Un0 [V oV UVA] [W cW UWA]; apply: clpnA => //; first split.
- by apply/open_subspaceP; exists V; rewrite // setIC UVA setIAC setIid.
- by apply/closed_subspaceP; exists W; rewrite // setIC UWA setIAC setIid.
- by rewrite UWA; exact: subIsetl.
Qed.

End Subspace.

. (A : set T) :=
  isPointed.Build (subspace A) point.

Global Instance { : topologicalType}
    ( : set T) ( : subspace A) :
  Filter (nbhs_subspace x) := nbhs_subspace_filter x.

Global Instance { : topologicalType}
    ( : set T) ( : subspace A) :
  ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x.

Definition { : Type} ( : set T) ( : T -> U)
  : subspace A -> U := f.
Arguments from_subspace {T U} A f.

Notation :=
  (continuous (from_subspace A f)) : classical_set_scope.

Arguments nbhs_subspaceP {T} A x.

Section SubspaceRelative.
Context { : topologicalType}.
Implicit Types (U : topologicalType) (A B : set T).

Lemma ( : T) :
  A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A).

Proof.

rewrite /= => AB; case: (nbhs_subspaceP A); case: (nbhs_subspaceP B).
- by move=> ? ?; apply: within_subset => //=; exact: (nbhs_filter x).
- by move=> ? /AB.
- by move=> Bx ? W /nbhs_singleton /(_ Bx) ? ? ->.
- by move=> ? ?.
Qed.

Lemma {} ( : T -> U) :
A `<=` B ->
{within B, continuous f} -> {within A, continuous f}.

Proof.

by move=> ? ctsF ? ? ?; apply: (@nbhs_subspace_subset A B) => //; exact: ctsF.
Qed.

Lemma ( : T) : nbhs (x : subspace setT) = nbhs x.

Proof.

have [_|] := nbhs_subspaceP [set: T]; last by cbn.
rewrite eqEsubset withinE; split => [W [V nbhsV]|W ?]; last by exists W.
by rewrite 2!setIT => ->.
Qed.

Lemma {} ( : T -> U) ( : T) :
A x -> {for x, continuous f} -> {for x, continuous (f : subspace A -> U)}.

Proof.

rewrite /continuous_at /prop_for => inA ctsf.
have [_|//] := nbhs_subspaceP A x.
by apply: (cvg_trans _ ctsf); apply: cvg_fmap2; exact: cvg_within.
Qed.

Lemma {} ( : T -> U) :
{in A, continuous f} -> {within A, continuous f}.

Proof.

rewrite continuous_subspace_in ?in_setP => ctsf t At.
by apply: continuous_subspaceT_for => //=; exact: ctsf.
Qed.

Lemma {} ( : T -> U) :
continuous f -> {within A, continuous f}.

Proof.

move=> ctsf; rewrite continuous_subspace_in => ? ?.
exact: continuous_in_subspaceT.
Qed.

Lemma {} : {within A, continuous (@cst T U u)}.

Proof.

by apply: continuous_subspaceT; exact: cst_continuous. Qed.

Lemma {} ( : T -> U) :
open A -> {within A, continuous f} = {in A, continuous f}.

Proof.

rewrite openE continuous_subspace_in /= => oA; rewrite propeqE ?in_setP.
by split => + x /[dup] Ax /oA Aox => /(_ _ Ax);
rewrite /continuous_at -(nbhs_subspace_interior Aox).
Qed.

Lemma {} ( : T -> U) : open A ->
{in A, continuous f} <-> open `<=` image_set_system A f open.

Proof.

move=> oA; rewrite -continuous_open_subspace// continuousP.
by under eq_forall do rewrite -open_setSI//.
Qed.

Lemma {} ( : T -> U) : closed A -> closed B ->
{within A, continuous f} -> {within B, continuous f} ->
{within A `|` B, continuous f}.

Proof.

move=> ? ? ctsA ctsB; apply/continuous_closedP => W oW.
case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsA => V1 cV1 V1W.
case/continuous_closedP/(_ _ oW)/closed_subspaceP: ctsB => V2 cV2 V2W.
apply/closed_subspaceP; exists ((V1 `&` A) `|` (V2 `&` B)).
by apply: closedU; exact: closedI.
rewrite [RHS]setIUr -V2W -V1W eqEsubset; split=> t.
by case=> [[][]] ? ? [] ?; [left | left | right | right].
by case=> [][] ? ?; split=> []; [left | left | right | right].
Qed.

Lemma {} ( : set U) ( : {fun A >-> B}) :
{within A, continuous f} -> continuous (f : subspace A -> subspace B).

Proof.

move=> /continuousP ctsf; apply/continuousP => O /open_subspaceP [V oV VBOB].
rewrite -open_subspaceIT; apply/open_subspaceP.
case/open_subspaceP: (ctsf _ oV) => W oW fVA; exists W => //.
rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //.
- by have /[!VBOB]-[] : (V `&` B) (f x) by split => //; exact: funS.
- by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS.
Qed.

Lemma {} ( : T -> U) : {within set0, continuous f}.

Proof.

move=> x Q /=.
by case: (nbhs_subspaceP (@set0 T) x) => // _ /nbhs_singleton /= ? ? ->.
Qed.

Lemma {} ( : T) ( : T -> U) :
{within [set a], continuous f}.

Proof.

move=> x Q /=.
case: (nbhs_subspaceP [set a] x); last by move=> _ /nbhs_singleton /= ? ? ->.
by move=> -> /nbhs_singleton ?; apply: nearW => ? ->.
Qed.

End SubspaceRelative.

Section SubspaceUniform.
Local Open Scope relation_scope.
Context { : uniformType} ( : set X).

Definition :=
filter_from (@entourage X)
(fun => [set | (xy.1 = xy.2) \/ (A xy.1 /\ A xy.2 /\ E xy)]).

Let : Filter subspace_ent.

Proof.

apply: filter_from_filter; first by (exists setT; exact: filterT).
move=> P Q entP entQ; exists (P `&` Q); first exact: filterI.
move=> [x y] /=; case; first (by move=> ->; split=> /=; left).
by move=> [Ax [Ay [Pxy Qxy]]]; split=> /=; right.
Qed.

Let ( : set (subspace A * subspace A)) :
subspace_ent B -> diagonal `<=` B.

Proof.

by move=> + [x y]/diagonalP ->; case=> V entV; apply; left. Qed.

Let ( : set (subspace A * subspace A)) :
subspace_ent B -> subspace_ent B^-1.

Proof.

case=> V ? Vsub; exists V^-1; first exact: entourage_inv.
move=> [x y] /= G; apply: Vsub; case: G; first by (move=> <-; left).
by move=> [? [? Vxy]]; right; repeat split.
Qed.

Let ( : set (subspace A * subspace A)) :
subspace_ent C -> exists2 , subspace_ent B & B \; B `<=` C.

Proof.

case=> E entE Esub.
exists [set | xy.1 = xy.2 \/ A xy.1 /\ A xy.2 /\ split_ent E xy].
  by exists (split_ent E).
move=> [x y] [z /= Ez zE] /=; case: Ez; case: zE.
- by move=> -> ->; apply: Esub; left.
- move=> [ ? []] ? G xy; subst; apply: Esub; right; repeat split => //=.
  by apply: entourage_split => //=; first exact: G; exact: entourage_refl.
- move=> -> [ ? []] ? G; apply: Esub; right; repeat split => //=.
  by apply: entourage_split => //=; first exact: G; exact: entourage_refl.
- move=> []? []? ?[]?[]??; apply: Esub; right; repeat split => //=.
  by apply: subset_split_ent => //; exists z.
Qed.

Let : @nbhs _ (subspace A) = nbhs_ subspace_ent.

Proof.

pose EA := [set | xy.1 = xy.2 \/ A xy.1 /\ A xy.2].
have entEA : subspace_ent EA.
  exists setT; first exact: filterT.
  by move=> [??] /= [ ->|[?] [?]];[left|right].
rewrite funeq2E=> x U.
case: (@nbhs_subspaceP X A x); rewrite propeqE; split => //=.
- rewrite withinE; case=> V /[dup] nbhsV => [/nbhsP [E entE Esub] UV].
  exists [set | xy.1 = xy.2 \/ A xy.1 /\ A xy.2 /\ E xy].
    by exists E => //= [[? ?]] /= [->| [? []]//]; exact: entourage_refl.
  move=> y /= /xsectionP/= -[<-{y}|].
    suff : (U `&` A) x by case.
    by rewrite UV; split => //; exact: (@nbhs_singleton X).
  case=> _ [Ay Ey]; suff : (U `&` A) y by case.
  by rewrite UV; split => //; exact/Esub/xsectionP.
- move=> [] W [E eentE subW] subU //=.
  near=> w; apply/subU/xsectionP/subW; right; repeat split => //=.
    exact: (near (withinT _ (@nbhs_filter X _))).
  by near: w; apply/nbhsP; exists E => // y /xsectionP.
- move=> //= Ux; exists EA => //.
  by move=> y /xsectionP => -[|[]] //= <-; exact: Ux.
- rewrite //= => [[W [W' entW' subW] subU]] ? ->.
  by apply/subU/xsectionP/subW; left.
Unshelve. all: by end_near. Qed.

..Build (subspace A)
  Filter_subspace_ent subspace_uniform_entourage_diagonal
  subspace_uniform_entourage_inv subspace_uniform_entourage_split_ex
  subspace_uniform_nbhsE.

End SubspaceUniform.

Section SubspacePseudoMetric.
Context { : numDomainType} { : pseudoMetricType R} ( : set X).
Implicit Type e : R.

Definition ( : subspace A) ( : R) :=
  if x \in A then A `&` ball (x : X) r else [set x].

Let : 0 < e -> subspace_ball x e x.

Proof.

rewrite /subspace_ball; case: ifP => //= /asboolP ? ?.
by split=> //; exact: ballxx.
Qed.

Let : subspace_ball x e y -> subspace_ball y e x.

Proof.

rewrite /subspace_ball; case: ifP => //= /asboolP ?.
by move=> [] Ay /ball_sym yBx; case: ifP => /asboolP.
by move=> ->; case: ifP => /asboolP.
Qed.

Let :
subspace_ball x e1 y -> subspace_ball y e2 z -> subspace_ball x (e1 + e2) z.

Proof.

rewrite /subspace_ball; (repeat case: ifP => /asboolP).
- by move=>?? [??] [??]; split => //=; apply: ball_triangle; eauto.
- by move=> ?? [??] ->.
- by move=> + /[swap] => /[swap] => ->.
- by move=> _ _ -> ->.
Qed.

Let : @entourage (subspace A) = entourage_ subspace_ball.

Proof.

rewrite eqEsubset; split; rewrite /subspace_ball.
  move=> U [W + subU]; rewrite -entourage_ballE => [[eps] nneg subW].
  exists eps => //; apply: (subset_trans _ subU).
  move=> [x y] /=; case: ifP => /asboolP ?.
    by move=> [Ay xBy]; right; repeat split => //; exact: subW.
  by move=> ->; left.
move=> E [eps nneg subE]; exists [set | ball (xy.1 : X) eps xy.2].
  by rewrite -entourage_ballE; exists eps.
move=> [x y] /= [->|[]Ax []Ay xBy]; apply: subE => //=.
  by case: ifP => /asboolP; split => //; exact: ballxx.
by case: ifP => /asboolP.
Qed.

.
  .Build R (subspace A) subspace_ball
    subspace_pm_ball_center subspace_pm_ball_sym subspace_pm_ball_triangle
    subspace_pm_entourageE.

Lemma ( : subspace A) ( : subspace A) :
  ball x r y = subspace_ball x r y.

Proof.

by []. Qed.

End SubspacePseudoMetric.

Section SubspaceInitial.
Context { : topologicalType} { : choiceType} ( : U -> T).

Lemma ( : set (initial_topology f)) :
open A -> open (f @` A : set (subspace (range f))).

Proof.

case=> B oB <-; apply/open_subspaceP; exists B => //; rewrite eqEsubset.
split => z [] /[swap]; first by case=> w _ <- ?; split; exists w.
by case=> w _ <- [v] ? <-.
Qed.

End SubspaceInitial.

Lemma { : topologicalType} ( : T -> U) :
{within A, continuous f} -> compact A -> compact (f @` A).

Proof.

move=> fcont Aco F FF FfA; set G := filter_from F (fun => A `&` f @^-1` C).
have GF : ProperFilter G.
  apply: (filter_from_proper (filter_from_filter _ _)).
  - by exists (f @` A).
  - by move=> C1 C2 F1 F2; exists (C1 `&` C2); [exact: filterI|move=> ? [? []]].
  - by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; exists p.
move: Aco; rewrite -[A]setIid => /compact_subspaceIP; rewrite setIid.
case /(_ G); first by exists (f @` A) => // ? [].
move=> /= p [Ap clsGp]; exists (f p); split; first exact/imageP.
move=> B C FB /fcont p_Cf.
have : image_set_system A f G B by exists B.
by move=> /clsGp /(_ p_Cf) [q [[]]]; exists (f q).
Qed.

Lemma { : topologicalType}
( : set T) ( : T -> U) :
connected A -> {within A, continuous f} -> connected (f @` A).

Proof.

move=> cA cf; apply: contrapT => /connectedPn[E [E0 fAE sE]].
set AfE := fun => (A `&` f @^-1` E b) : set (subspace A).
suff sAfE : separated (AfE false) (AfE true).
  move: cA; apply/connectedPn; exists AfE; split; last (rewrite /AfE; split).
  - move=> b; case: (E0 b) => /= u Ebu.
    have [t Et ftu] : (f @` A) u by rewrite fAE; case: b Ebu; [right|left].
    by exists t; split => //=; rewrite /preimage ftu.
  - by rewrite -setIUr -preimage_setU -fAE; exact/esym/setIidPl/preimage_image.
  + rewrite -{2}(setIid A) ?setIA -(@closure_subspaceW _ A); first by move=> ?[].
    by rewrite -/(AfE false) -setIA -/(AfE true); case: sAfE.
  + rewrite -{1}(setIid A) setIC ?setIA -(@closure_subspaceW _ A) => [? []//|].
    by rewrite -/(AfE true) -setIA -/(AfE false) setIC; case: sAfE.
suff cI0 b : closure (AfE b) `&` AfE (~~ b) = set0.
  by rewrite /separated cI0 setIC cI0.
have [fAfE cEIE] :
    f @` AfE (~~ b) = E (~~ b) /\ closure (E b) `&` E (~~ b) = set0.
  split; last by case: sE => ? ?; case: b => //; rewrite setIC.
  rewrite eqEsubset; split => [|u Ebu].
    apply: (subset_trans sub_image_setI).
    by apply: subIset; right; exact: image_preimage_subset.
  have [t [At ftu]] : exists , A t /\ f t = u.
    suff [t At ftu] : (f @` A) u by exists t.
    by rewrite fAE; case: b Ebu; [left|right].
  by exists t => //; split => //=; rewrite /preimage ftu.
have ? : f @` closure (AfE b) `<=` closure (E b).
  have /(@image_subset _ _ f) : closure (AfE b) `<=` f @^-1` closure (E b).
    have /closure_id -> : closed (f @^-1` closure (E b) : set (subspace A)).
      by apply: preimage_closed => //; exact: closed_closure.
    apply: closureS.
    have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b).
    by apply: subset_trans A0cA0; apply: subIset; right.
  by move/subset_trans; apply; exact: image_preimage_subset.
apply/nonemptyPn => -[t [AfEb AfENb]].
have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0.
  by rewrite fAfE; exact: subsetI_eq0 cEIE.
by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t.
Qed.

Lemma { : topologicalType} ( : X -> Y) :
  continuous f <->
  forall : X, \forall \near powerset_filter_from (nbhs x),
    {within U, continuous f}.

Proof.

split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact.
move=> + x => /(_ x)/near_powerset_filter_fromP.
case; first by move=> ? ?; exact: continuous_subspaceW.
move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U.
move: nbhsU; rewrite nbhsE => -[] W [oW Wx WU] /(_ W).
by move/(_ (continuous_subspaceW WU wctsf)); apply => //; exists W.
move/nbhs_singleton: nbhsU; move: x; apply/in_setP.
by rewrite -continuous_open_subspace.
Unshelve. end_near. Qed.

Lemma { : topologicalType} ( : T -> U) :
continuous f <-> {within setT, continuous f}.

Proof.

by split => + x K nfK=> /(_ x K nfK); rewrite nbhs_subspaceT. Qed.

Section subspace_product.
Context { : topologicalType} ( : set X) ( : set Y) .

Lemma : (A `*` B) x ->
nbhs (x : subspace (A `*` B)) = @nbhs _ (subspace A * subspace B)%type x.

Proof.

case: x => a b [/= Aa Bb]; rewrite /nbhs/= -nbhs_subspace_in//.
rewrite funeqE => U /=; rewrite propeqE; split; rewrite /nbhs /=.
  move=> [[P Q]] /= [nxP nyQ] PQABU; exists (P `&` A, Q `&` B).
    by split; apply/nbhs_subspace_ex => //=; [exists P | exists Q];
      rewrite // -setIA setIid.
  by case=> p q [[/= Pp Ap [Qq Bq]]]; exact: PQABU.
move=> [[P Q]] /= [/(nbhs_subspace_ex _ Aa) [P' P'a PPA]].
move/(nbhs_subspace_ex _ Bb) => [Q' Q'a QQB PQU].
exists (P', Q') => //= -[p q] [P'p Q'q] [Ap Bq]; apply: PQU; split => /=.
  by have [] : (P `&` A) p by rewrite PPA.
by have [] : (Q `&` B) q by rewrite QQB.
Qed.

Lemma ( : X * Y -> Z) :
{in A `*` B, continuous (f : subspace A * subspace B -> Z)} <->
{within A `*` B, continuous f}.

Proof.

by split; rewrite continuous_subspace_in => + x ABx U nfxU => /(_ x ABx U nfxU);
rewrite nbhs_prodX_subspace_inE//; move/set_mem: ABx.
Qed.

End subspace_product.

( )
.
    (A : set X) (B : set Y) :=
  { of @isFun (subspace A) Y A B f & @Continuous (subspace A) Y f }.

#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `continuousSubspaceType`")]
Notation := continuousSubspaceType.
#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `ContinuousSubspace`")]
Notation A B := (ContinuousSubspace A B).

Section continuous_fun_comp.
Context { : topologicalType} ( : set X) ( : set Y) ( : set Z)
  { : continuousSubspaceType A B} { : continuousSubspaceType B C}.

#[local] Lemma : continuous (g \o f : subspace A -> Z).

Proof.

move=> x; apply: continuous_comp; last exact: continuous_fun.
exact/subspaceT_continuous/continuous_fun.
Qed.

End continuous_fun_comp.

Section continuous_patch.
Context { : topologicalType} ( : set U) ( : U -> V).
Hypotheses ( : {within A, continuous f})
  ( : {within B, continuous g})
  ( : closed A)
  ( : closed B)
  ( : forall , x \in A `&` B -> f x = g x).

Lemma : {within A `|` B, continuous (patch g A f)}.

Proof.

pose gAf := patch g A f.
apply: withinU_continuous => //.
- suff : {in A, f =1 gAf} by move/subspace_eq_continuous; exact.
  by rewrite /gAf /patch => r ->.
- suff : {in B, g =1 gAf} by move/subspace_eq_continuous; exact.
  move=> r rB; rewrite /gAf /patch; case: ifPn => // rA.
  by apply/esym/AB_fg; rewrite in_setI rA.
Qed.

End continuous_patch.

Definition { : uniformType} ( : set X) :
    set (subspace A * subspace A) :=
  [set | (A z.1 /\ A z.2) \/ z.1 = z.2].
Arguments subdiagonal {X} _.

Lemma { : uniformType} ( : set X) :
  @entourage (subspace A) (subdiagonal A).

Proof.

rewrite -[entourage (subdiagonal A)]/(subspace_ent A (subdiagonal A)).
rewrite /subspace_ent /filter_from /=.
exists setT; first exact: entourageT.
move=> z /= [z12|[A1 [A2 _]]].
- by rewrite /subdiagonal/= z12; right.
- by rewrite /subdiagonal/=; left.
Qed.

Section HeineCantorUniform.
Context { : uniformType}.

Let ( : set X) ( : X -> Y) ( : set (Y * Y))
    ( : subspace A * subspace A) ( : subspace A) : Prop :=
  i.1 = x -> (map_pair f @^-1` E) i.

Let ( : set X) ( : X -> Y) ( : set (Y * Y)) :
  {within A, continuous f} -> entourage E ->
  forall : subspace A,
  \forall \near a & \near entourage, unif_cont_at f E z i.

Proof.

move=> cf entE.
pose E' := split_ent E.
pose W : set (Y * Y) := E' `&` E'^-1%relation.
have entW : @entourage Y W by apply: entourage_invI; exact: entourage_split_ent.
move=> a.
have /nbhsP [/= C entC Csub] :=
  cf a (xsection W (f a)) (nbhs_entourage (f a) entW).
pose D := split_ent C.
have entD : entourage D by exact: entourage_split_ent.
have near_Da : \forall \near a, D (a, x).
  move: entD => /(nbhs_entourage a).
  rewrite -filter_from_entourageE => -[/= F entF FDa].
  near do apply/set_mem/FDa/xsectionP.
  by apply: cvg_entourage; [exact: cvg_id|exact: entF].
near=> x z => /=.
have Dax : D (a, x) by near: x; exact: near_Da.
have Dz : D z by near: z; exact: entD.
move=> /= z1x.
have {Dax}Daz1 : D (a, z.1) by rewrite z1x.
have {Dz}Caz2 : C (a, z.2).
  apply: (entourage_split x entC); rewrite -/D.
    by rewrite -z1x; exact: Daz1.
  by rewrite -z1x -surjective_pairing; exact: Dz.
have Caz1 : C (a, z.1) by exact: (split_ent_subset entC).
have Waz1 : W (f a, f z.1).
  suff : (f @^-1` xsection W (f a)) z.1 by rewrite /= => /xsectionP.
  by apply: Csub => //; exact/xsectionP.
have Waz2 : W (f a, f z.2).
  suff : (f @^-1` xsection W (f a)) z.2 by rewrite /= => /xsectionP.
  by apply: Csub => //; exact/xsectionP.
move: Waz1 Waz2 => [_ E'az1] [E'az2 _].
exact: (entourage_split (f a) entE).
Unshelve. all: end_near. Qed.

Lemma ( : set X) ( : X -> Y) :
compact A -> {within A, continuous f} ->
@unif_continuous (subspace A) Y f.

Proof.

move=> cA cf E entE.
rewrite -[nbhs _ E]/(subspace_ent A
  [set : subspace A * subspace A | E (f xy.1, f xy.2)]).
have compactA_subspace : @compact (subspace A) A.
  rewrite -[A](@setTI (subspace A)).
  have [_] := @compact_subspaceIP X A setT.
  by rewrite setTI; exact.
have A_unif_cont_at : \forall \near entourage, A `<=` @unif_cont_at A f E V.
  have := (@compact_near_coveringP (subspace A) A).1 compactA_subspace.
  move/(_ _ entourage (@unif_cont_at A f E)).
  by apply=> a Aa; exact/unif_cont_atP.
pose W : set (subspace A * subspace A) := [set | A `<=` unif_cont_at f E z].
have entW : entourage W by [].
apply: (@filterS _ _ _ (W `&` subdiagonal A)); last first.
  by apply: filterI => //; exact: ent_subdiagonal.
move=> [x y] /= [Wxy] [[/= Ax Ay]|/= xy].
- exact: Wxy _ Ax _.
- rewrite xy.
  exact: entourage_refl.
Qed.

End HeineCantorUniform.

Files

Module mathcomp.analysis.topology_theory.subspace_topology