Module mathcomp.analysis.topology_theory.topology_structure

From HB Require Import structures.
From mathcomp Require Import boot order algebra finmap.
From mathcomp Require Import all_classical.
From mathcomp Require Export filter.

# Basic topological notions This file develops tools for the manipulation of basic topological notions. The development of topological notions builds on "filtered types" by extending the hierarchy. In the identifiers, "nbhs" is an abbreviation for "neighborhoods". ## Mathematical structures ### Topology `topologicalType` : interface type for topological space structure : The HB class is `Topological`. `subTopologicalType S` : join of `SubNbhs` and `Topological` where `S` has type `pred V` with `V` : a `topologicalType` : The HB class is `SubTopological`. `ptopologicalType` : a pointed `topologicalType` `open` : set of open sets `closed` : set of closed sets `clopen U` : `U` is both open and closed `open_nbhs p` : set of open neighbourhoods of `p` `dense S` : the set `S : set T` is dense in `T`, with `T` of type `topologicalType` `basis B` : a family of open sets that converges to each point `separable_set A` : `A : set T` admits a countable dense subset `separable T` : `separable_set T [set: T]` `second_countable T` : `T` has a countable basis `[locally P]` : `forall a, A a -> G (within A (nbhs x))` if `P` is convertible to : `G (globally A)` `U°` : all of the points which are locally in `U`, i.e., the largest open set : contained in `U` : This is a notation for `interior U`. `closure U` : the smallest closed set containing `U` `regopen U` : `U` is regular open, i.e., equal to the interior of its closure `regclosed U` : `U` is regular closed, i.e., equal to the closure of its interior `open_of_nbhs B` : the open sets induced by neighborhoods `nbhs_of_open B` : the neighborhoods induced by open sets `x^'` : set of neighbourhoods of `x` where `x` is excluded : (a "deleted neighborhood") `limit_point E` : the set of limit points of E `isolated A` : the set of isolated points of `A` `continuousType` : type of continuous functions : The HB structures is `Continuous`. `mkcts f_cts` : object of type `continuousType` corresponding to the function `f` : (`f_cts : continuous f`) ### Factories ``` Nbhs_isNbhsTopological == factory for a topology defined by a filter It builds the mixin for a topological space from the properties of nbhs and hence assumes that the carrier is a filterType. isOpenTopological == factory for a topology defined by open sets It builds the mixin for a topological space from the properties of open sets, nbhs_of_open must be used to declare a filterType. isBaseTopological == factory for a topology defined by a base of open sets It builds the mixin for a topological space from the properties of a base of open sets; the type of indices must be a pointedType isSubBaseTopological == factory for a topology defined by a subbase of open sets It builds the mixin for a topological space from a subbase of open sets b indexed on domain D ```

Reserved Notation "A °" (format "A °").
Reserved Notation "[ 'locally' P ]" (format "[ 'locally' P ]").
Reserved Notation "x ^'" (format "x ^'").

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Topological spaces

. () T := {
  open : set_system T;
  nbhs_pfilter_subproof : forall : T, ProperFilter (nbhs p) ;
  nbhsE_subproof : forall : T, nbhs p =
    [set : set T | exists : set T, [/\ open B, B p & B `<=` A] ] ;
  openE_subproof : open = [set : set T | A `<=` nbhs^~ A ]
}.

()
.
  { of Nbhs T & Nbhs_isTopological T}.

()
.
  { of PointedNbhs T & Nbhs_isTopological T}.

()
.
  { of BiPointed X & Topological X }.

()
. ()
  (S : pred V) := { of SubNbhs V S U & Topological U}.

Section Topological1.
Context { : topologicalType}.

Definition ( : T) ( : set T) := open A /\ A p.

Global Instance ( : T) : ProperFilter (nbhs p).

Proof.

by apply: nbhs_pfilter_subproof; case: T p => ? []. Qed.

Typeclasses Opaque nbhs.
Lemma ( : T) : Filter (nbhs p).

Proof.

exact: (@nbhs_pfilter). Qed.

Canonical ( : T) := FilterType (nbhs x) (@nbhs_filter x).

Lemma ( : T) :
nbhs p = [set : set T | exists2 : set T, open_nbhs p B & B `<=` A].

Proof.

have -> : nbhs p = [set : set T | exists , [/\ open B, B p & B `<=` A] ].
exact: nbhsE_subproof.
by rewrite predeqE => A; split=> [[B [?]]|[B[]]]; exists B.
Qed.

Lemma ( : T) ( : set T) : open_nbhs p A = (open A /\ nbhs p A).

Proof.

by rewrite nbhsE propeqE; split=> [[? ?]|[? [B [? ?] BA]]]; split => //;
[exists A | exact: BA].
Qed.

Definition ( : set T) := (@nbhs _ T)^~ A.

Local Notation := (interior A).

Lemma ( : set T) : A° `<=` A.

Proof.

by move=> p; rewrite /interior nbhsE => -[? [? ?]]; apply.
Qed.

Lemma : open = [set : set T | A `<=` A°].

Proof.

exact: openE_subproof. Qed.

Lemma ( : T) ( : set T) : nbhs p A -> A p.

Proof.

by rewrite nbhsE => - [? [_ ?]]; apply. Qed.

Lemma ( : T) ( : set T) : nbhs p A -> nbhs p A°.

Proof.

rewrite nbhsE /open_nbhs openE => - [B [Bop Bp] sBA].
by exists B => // q Bq; apply: filterS sBA _; apply: Bop.
Qed.

Lemma : open (set0 : set T).

Proof.

by rewrite openE. Qed.

Lemma : open (setT : set T).

Proof.

by rewrite openE => ??; apply: filterT. Qed.

Lemma : setI_closed (@open T).

Proof.

move=> A B; rewrite openE => Aop Bop p [Ap Bp].
by apply: filterI; [apply: Aop|apply: Bop].
Qed.

Lemma ( : Type) ( : set I) ( : I -> set T) :
(forall , D i -> open (f i)) -> open (\bigcup_( in D) f i).

Proof.

rewrite openE => fop p [i Di].
by have /fop fiop := Di; move/fiop; apply: filterS => ??; exists i.
Qed.

Lemma ( : (set T) ^nat) :
(forall , open (F i)) ->
forall , open (\bigcap_( < i) F j).

Proof.

move=> HU; elim; [rewrite bigcap_mkord big_ord0; apply: openT|move=> n IH].
by rewrite bigcap_mkord big_ord_recr -bigcap_mkord; apply: openI.
Qed.

Lemma : setU_closed (@open T).

Proof.

by move=> A B /[!openE] AA BB p [/AA|/BB]; apply: filterS => ? ?; [left|right].
Qed.

Lemma ( : set T) : open A -> (A `<=` B) = (A `<=` B°).

Proof.

rewrite openE => Aop; rewrite propeqE; split.
by move=> sAB p Ap; apply: filterS sAB _; apply: Aop.
by move=> sAB p /sAB /interior_subset.
Qed.

Lemma ( : set T) : open A°.

Proof.

rewrite openE => p; rewrite /interior nbhsE => - [B [Bop Bp]].
by rewrite open_subsetE //; exists B.
Qed.

Lemma ( : set I) ( : I -> set T) :
\bigcup_( in D) (f i)° `<=` (\bigcup_( in D) f i)°.

Proof.

move=> p [i Di]; rewrite /interior nbhsE => - [B [Bop Bp] sBfi].
by exists B => // ? /sBfi; exists i.
Qed.

Lemma ( : T) : open_nbhs p setT.

Proof.

by split=> //; apply: openT. Qed.

Lemma ( : T) : setI_closed (open_nbhs p).

Proof.

by move=> A B [Aop Ap] [Bop Bp]; split => //; exact: openI. Qed.

Lemma ( : T) ( : set T) : open_nbhs p A -> nbhs p A.

Proof.

by rewrite nbhsE => p_A; exists A. Qed.

Lemma ( : set T) : (A `&` B)° = A° `&` B°.

Proof.

rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []].
- by rewrite subsetI => // -[? ?]; split; exists B0.
- by move=> -[B0 ? ?] [B1 ? ?]; exists (B0 `&` B1);
[exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]].
Qed.

End Topological1.

Lemma { : topologicalType} ( : T -> Prop) ( : set T) :
open S -> {in S, forall , P x} -> {in S, forall , \forall \near x, P x0}.

Proof.

by move=> oS SP z /set_mem Sz; apply: in_nearW SP => //=; exact: open_nbhs_nbhs.
Qed.

#[global] Hint Extern 0 (Filter (nbhs _)) =>
  solve [apply: nbhs_filter] : typeclass_instances.
#[global] Hint Extern 0 (ProperFilter (nbhs _)) =>
  solve [apply: nbhs_pfilter] : typeclass_instances.

Global Instance { : topologicalType} :
  @Filter T^o (@nbhs T^o T x).

Proof.

apply: @nbhs_filter T x. Qed.

Global Instance { : topologicalType} :
@ProperFilter T^o (@nbhs T^o T x).

Proof.

exact: @nbhs_pfilter T x. Qed.

Reserved Notation "A ^°" (at level 1, format "A ^°").
Notation := (interior A) : classical_set_scope.
#[deprecated(since="mathcomp-analysis 1.10.0", note="use the notation instead ° instead of ^°")]
Notation := (A°) (only parsing).

Lemma ( : topologicalType) ( : S -> T) :
continuous f <-> forall , open A -> open (f @^-1` A).

Proof.

split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont.
move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA].
by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA].
Qed.

Lemma { : topologicalType} ( : T -> U) ( : set U) :
{in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).

Proof.

rewrite !openE => fcont Dop x /= Dfx.
by apply: fcont; [rewrite inE|exact: Dop].
Qed.

Lemma { : topologicalType} { : topologicalType}
( : set_system T) ( : T -> U) :
{for x, continuous f} -> F --> x -> f @ F --> f x.

Proof.

by move=> cf fx P /cf /fx. Qed.

Lemma ( : topologicalType) ( : T) ( : set T) :
(\forall \near x, P x0) -> \forall \near x, \forall \near x0, P x1.

Proof.

exact: nbhs_interior. Qed.

Lemma ( : topologicalType) ( : set T) ( : T) :
  (\forall \near x, (\forall \near x, P x1) -> Q x0) ->
  (\forall \near x, P x0) ->
  \forall \near x, Q x0.

Proof.

move=> PQ xP; near=> y; apply: (near PQ y) => //;
exact: (near (near_join xP) y).
Unshelve. all: by end_near. Qed.

Lemma { : Type} { : topologicalType}
  ( : set_system T) ( : Filter F)
  ( : T -> V) ( : V -> U) ( : V) :
  {for a, continuous h} ->
  f @ F --> a -> (h \o f) @ F --> h a.

Proof.

move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous).
exact: (cvg_comp _ h fa).
Qed.

Lemma { : Type} { : ptopologicalType} [ : set_system T]
  ( : Filter F) ( : T -> V) ( : V -> U) :
  (forall , f x @[ --> F] --> l -> {for l, continuous h}) ->
  cvg (f x @[ --> F]) -> cvg ((h \o f) x @[ --> F]).

Proof.

move=> ach /cvg_ex[l fxl]; apply/cvg_ex; exists (h l).
by apply: continuous_cvg => //; exact: ach.
Qed.

Lemma { : Type} { : topologicalType}
  ( : set_system T) ( : Filter F)
  ( : T -> V) ( : T -> W) ( : V -> W -> U) ( : V) ( : W) :
  h z.1 z.2 @[ --> (a, b)] --> h a b ->
  f @ F --> a -> g @ F --> b -> (fun => h (f x) (g x)) @ F --> h a b.

Proof.

move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous).
exact: (cvg_comp _ (fun => h x.1 x.2) (cvg_pair fa fb)).
Qed.

Lemma { : topologicalType}
  ( : T -> V) ( : V -> U) ( : T) ( : U) :
  {for f r, continuous h} ->
  (h \o f) x @[ --> r] --> l -> h x @[ --> f r] --> l.

Proof.

move=> frh hfrl X; rewrite nbhsE => -[Y [oY Yl]].
move/filterS; apply; apply: frh.
rewrite nbhsE; exists Y => //; split => //.
have /hfrl : nbhs l Y by exact: open_nbhs_nbhs.
by rewrite nbhsE => -[W [oW Wr]]; exact.
Qed.

Lemma ( : Type) ( : topologicalType)
( : U) ( : T -> U) ( : set_system T) { : Filter F} :
(\forall \near F, f x = l) -> f @ F --> l.

Proof.

move=> fFl P /=; rewrite !near_simpl => Pl.
by apply: filterS fFl => _ ->; exact: nbhs_singleton.
Qed.

Arguments cvg_near_cst {T U} l {f F FF}.

Lemma ( : Type) ( : ptopologicalType)
( : U) ( : T -> U) ( : set_system T) { : Filter F} :
(\forall \near F, f x = l) -> cvg (f @ F).

Proof.

by move=> /cvg_near_cst/cvgP. Qed.

Arguments is_cvg_near_cst {T U} l {f F FF}.

Lemma ( : topologicalType)
( : U) ( : T -> U) ( : T) :
(\forall \near x, f y = l) -> {for x, continuous f}.

Proof.

move=> eq_f_l; apply: cvg_near_cst; apply: filterS (eq_f_l) => y ->.
by rewrite (nbhs_singleton eq_f_l).
Qed.

Arguments near_cst_continuous {T U} l [f x].

Lemma ( : topologicalType) ( : U) ( : Type)
( : set_system T) { : Filter F} :
(fun _ : T => x) @ F --> x.

Proof.

by apply: cvg_near_cst; near=> x0. Unshelve. all: by end_near. Qed.

Arguments cvg_cst {U} x {T F FF}.
#[global] Hint Extern 0 (_ @ _ --> _) => solve [apply: cvg_cst] : core.

Lemma ( : ptopologicalType) ( : U) ( : Type)
( : set_system T) { : Filter F} :
cvg ((fun _ : T => x) @ F).

Proof.

exact: cvgP (cvg_cst _). Qed.

Arguments is_cvg_cst {U} x {T F FF}.
#[global] Hint Extern 0 (cvg (_ @ _)) => solve [apply: is_cvg_cst] : core.
#[global] Hint Extern 0 (cvgn (_ @ _)) => solve [apply: is_cvg_cst] : core.

Lemma { : topologicalType} ( : U) :
continuous (fun _ : T => x).

Proof.

by move=> t; exact: cvg_cst. Qed.

Lemma { : topologicalType} : continuous (@id T).

Proof.

by move=> t; exact: cvg_id. Qed.

Section within_topologicalType.
Context { : topologicalType} ( : set T).
Implicit Types B : set T.

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

Proof.

move=> Ax P AP; rewrite /within/=; near=> y; apply: AP.
Unshelve. all: by end_near. Qed.

Definition ( : set_system T -> Prop) & phantom Prop (P (globally A))
:= forall , A x -> P (within A (nbhs x)).
Local Notation := (@locally_of _ _ _ (Phantom _ P)).

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

Proof.

move=> Aox; rewrite eqEsubset; split; last exact: cvg_within.
rewrite ?nbhsE => W /= => [[B + BsubW]].
rewrite open_nbhsE => [[oB nbhsB]].
exists (B `&` A°); last by move=> t /= [] /BsubW + /interior_subset; apply.
rewrite open_nbhsE; split; first by apply: openI => //; exact: open_interior.
by apply: filterI => //; have := open_interior A; rewrite openE; exact.
Qed.

Lemma : Filter F -> A `<=` B -> within A F `=>` within B F.

Proof.

move=> FF AsubB W; rewrite /within/=; apply: filter_app; rewrite nbhs_simpl.
by apply: filterE => ? + ?; apply; exact: AsubB.
Qed.

Lemma : Filter F ->
within A F = [set | exists2 , F V & U `&` A = V `&` A].

Proof.

move=> FF; rewrite eqEsubset; split=> U.
move=> Wu; exists [set | A x -> U x] => //.
by rewrite eqEsubset; split => t [L R]; split=> //; apply: L.
move=> [V FV AU]; rewrite /within /prop_near1 nbhs_simpl/=; near=> w => Aw.
by have []// : (U `&` A) w; rewrite AU; split => //; apply: (near FV).
Unshelve. all: by end_near. Qed.

Lemma { : topologicalType} ( : set_system T) ( : T -> S) :
Filter F -> {in A, f =1 g} -> f @ within A F --> g @ within A F.

Proof.

move=> FF feq U /=; near_simpl; apply: filter_app.
rewrite ?nbhs_simpl; near_simpl; near=> w; rewrite (feq w) // inE.
exact: (near (withinT A FF) w).
Unshelve. all: by end_near. Qed.

End within_topologicalType.

Notation := (@locally_of _ _ _ (Phantom _ P)).

Topology defined by a filter

. T := {
  nbhs_filter : forall : T, ProperFilter (nbhs p);
  nbhs_singleton : forall ( : T) ( : set T), nbhs p A -> A p;
  nbhs_nbhs : forall ( : T) ( : set T), nbhs p A -> nbhs p (nbhs^~ A);
}.

. T.

Definition := [set : set T | A `<=` nbhs^~ A].

Let ( : T) :
  nbhs p = [set | exists , [/\ open_of_nbhs B, B p & B `<=` A] ].

Proof.

rewrite predeqE => A; split=> [p_A|]; last first.
move=> [B [Bop Bp sBA]]; apply: filterS sBA _; last exact: Bop.
exact/nbhs_filter.
exists (nbhs^~ A); split=> //; first by move=> ?; apply: nbhs_nbhs.
by move=> q /nbhs_singleton.
Qed.

Let : open_of_nbhs = [set : set T | A `<=` nbhs^~ A].

Proof.

by []. Qed.

..Build T
nbhs_filter nbhsE_subproof openE_subproof.

..

Topology defined by open sets

Definition ( : Type) ( : set_system T) ( : T) ( : set T) :=
  exists , [/\ op B, B p & B `<=` A].

. T := {
  op : set_system T ;
  opT : op setT ;
  opI : setI_closed op ;
  op_bigU : forall ( : Type) ( : I -> set T), (forall , op (f i)) ->
    op (\bigcup_ f i)
}.

. T.

..Build T (nbhs_of_open op).

Let ( : T) : ProperFilter (nbhs p).

Proof.

apply: Build_ProperFilter_ex.
  by move=> A [B [_ Bp sBA]]; exists p; apply: sBA.
split; first by exists setT; split=> [|//|//]; exact: opT.
  move=> A B [C [Cop Cp sCA]] [D [Dop Dp sDB]].
  exists (C `&` D); split=> //; first exact: opI.
  by move=> q [/sCA Aq /sDB Bq].
move=> A B sAB [C [Cop p_C sCA]].
by exists C; split=> //; apply: subset_trans sAB.
Qed.

Let ( : T) :
nbhs p = [set | exists , [/\ op B, B p & B `<=` A] ].

Proof.

by []. Qed.

Let : op = [set : set T | A `<=` nbhs^~ A].

Proof.

rewrite predeqE => A; split=> [Aop p Ap|Aop].
by exists A; split=> //; split.
suff -> : A = \bigcup_( : { : set T & op B /\ B `<=` A}) projT1 B.
by apply: op_bigU => B; have [] := projT2 B.
rewrite predeqE => p; split=> [|[B _ Bp]]; last by have [_] := projT2 B; apply.
by move=> /Aop [B [Bop Bp sBA]]; exists (existT _ B (conj Bop sBA)).
Qed.

..Build T
nbhs_pfilter_subproof nbhsE_subproof openE_subproof.

..

Definition ( : Type) ( : Type) ( : set I) ( : I -> set T) :=
[set \bigcup_( in D') b i | in subset^~ D].

#[deprecated(since="mathcomp-analysis 1.17.0", use=openU_from)]
Notation := openU_from (only parsing).

Topology defined by a base of open sets

. T := {
  I : pointedType ;
  D : set I ;
  b : I -> set T ;
  b_cover : \bigcup_( in D) b i = setT ;
  b_join : forall , D i -> D j -> b i t -> b j t ->
    exists , [/\ D k, b k t & b k `<=` b i `&` b j]
}.

. T.

Local Notation := (openU_from D b).

Let : openU_from setT.

Proof.

exists D => //; exact: b_cover. Qed.

Let : setI_closed openU_from.

Proof.

move=> A B [DA sDAD AeUbA] [DB sDBD BeUbB].
have ABU t : (A `&` B) t ->
  exists , [/\ D it, b it t & b it `<=` A `&` B].
  move=> [At Bt].
  have [iA [DiA biAt sbiA]] : exists , [/\ D i, b i t & b i `<=` A].
    move: At; rewrite -AeUbA => - [i DAi bit]; exists i.
    by split => //; [exact: sDAD|exact: bigcup_sup].
  have [iB [DiB biBt sbiB]] : exists , [/\ D i, b i t & b i `<=` B].
    move: Bt; rewrite -BeUbB => - [i DBi bit]; exists i.
    by split=> //; [exact: sDBD|exact: bigcup_sup].
  have [i [Di bit sbiAB]] := b_join DiA DiB biAt biBt.
  by exists i; split=> // s /sbiAB [/sbiA ? /sbiB].
set Dt := fun => [set | [/\ D it, b it t & b it `<=` A `&` B]].
exists [set get (Dt t) | in A `&` B].
  by move=> _ [t ABt <-]; have /ABU/getPex [] := ABt.
rewrite predeqE => t; split=> [[_ [s ABs <-] bDtst]|ABt].
  by have /ABU/getPex [_ _] := ABs; exact.
by exists (get (Dt t)); [exists t| have /ABU/getPex [?]:= ABt].
Qed.

Let ( : Type) ( : I0 -> set T) :
(forall , openU_from (f i)) -> openU_from (\bigcup_ f i).

Proof.

set fop := fun => [set | Dj `<=` D /\ f j = \bigcup_( in Dj) b i].
exists (\bigcup_ get (fop j)).
  move=> i [j _ fopji].
  suff /getPex [/(_ _ fopji)] : exists , fop j Dj by [].
  by have [Dj] := H j; exists Dj.
rewrite predeqE => t; split=> [[i [j _ fopji bit]]|[j _]].
  exists j => //; suff /getPex [_ ->] : exists , fop j Dj by exists i.
  by have [Dj] := H j; exists Dj.
have /getPex [_ ->] : exists , fop j Dj by have [Dj] := H j; exists Dj.
by move=> [i]; exists i => //; exists j.
Qed.

..Build T
  openU_fromT openU_fromI openU_from_bigU.

..

. T := {
  I : pointedType ;
  D : set I ;
  b : I -> set T
}.

. T.

Local Notation := (open_finI_from D b).

Let : \bigcup_( in finI_from) A = setT.

Proof.

rewrite predeqE => t; split=> // _; exists setT => //.
by exists fset0 => //; rewrite predeqE.
Qed.

Let : finI_from A -> finI_from B -> A t -> B t ->
exists , [/\ finI_from k, k t & k `<=` A `&` B].

Proof.

move=> [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt.
exists (A `&` B); split => //.
exists (DA `|` DB)%fset; first by move=> i /fsetUP [/sDAD|/sDBD].
rewrite predeqE => s; split=> [Ifs|[As Bs] i /fsetUP].
  split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite /= inE DAi.
  by rewrite -BeIbB => i DBi; apply: Ifs; rewrite /= inE DBi orbC.
by move=> [DAi|DBi];
  [have := As; rewrite -AeIbA; apply|have := Bs; rewrite -BeIbB; apply].
Qed.

..Build T
finI_from_cover finI_from_join.

..

deleted neighborhood

Definition { : topologicalType} ( : T) :=
within (fun => y != x) (nbhs x).
Notation := (dnbhs x) : classical_set_scope.

Lemma { : topologicalType} ( : T) :
\forall \near nbhs p^', x != p.

Proof.

exact: withinT. Qed.

#[global] Hint Extern 0 (\forall \near nbhs _^', is_true (x != _)) =>
solve [apply: nbhs_dnbhs_neq] : core.

Lemma { : topologicalType} ( : T) : x^' `=>` nbhs x.

Proof.

exact: cvg_within. Qed.

Lemma ( : topologicalType) ( : T) :
nbhs x = x^' `&` principal_filter x.

Proof.

rewrite predeqE => A; split=> [x_A|[+ Ax]].
by split; [exact: nbhs_dnbhs|apply/principal_filterP; exact: nbhs_singleton].
rewrite /dnbhs !nbhsE => -[B [oB x_B sBA]]; exists B => //.
by move=> y /sBA Ay; case: (eqVneq y x) => [->|//]; exact/principal_filterP.
Qed.

Global Instance { : topologicalType} ( : T) : Filter x^'.

Proof.

exact: within_filter. Qed.

#[global] Typeclasses Opaque dnbhs.

Canonical ( : topologicalType)  ( : T) :=
  FilterType x^' (dnbhs_filter _).

Lemma ( : Type) ( : T -> U):
  forall ( : set_system T), G `=>` F -> f @ G `=>` f @ F.

Proof.

by move=> F G H A fFA ; exact: H (preimage f A) fFA. Qed.

Lemma { } { : T -> U} ( : set_system T) { : (Filter F) }
( : set_system U) ( : set T) : (f @ F) --> G -> (f @ within D F) --> G.

Proof.

exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed.

Lemma {} { : ptopologicalType} ( : T -> U) ( : set_system T)
( : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F).

Proof.

by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_filter.
Qed.

meets

Lemma { : topologicalType} ( : set_system T) ( : T) :
F `#` nbhs x = F `#` open_nbhs x.

Proof.

rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|].
by move=> P A B {}/P P; rewrite nbhsE => -[B' /P + sB]; apply: subsetI_neq0.
Qed.

Lemma { : topologicalType} ( : set_system T) ( : T) :
nbhs x `#` F = open_nbhs x `#` F.

Proof.

by rewrite meetsC meets_openr meetsC. Qed.

Closed sets in topological spaces

Section Closed.
Context { : topologicalType}.

Definition ( : set T) :=
[set : T | forall , nbhs p B -> A `&` B !=set0].

Lemma : closure A = [set | globally A `#` nbhs p].

Proof.

by under eq_fun do rewrite meets_globallyl. Qed.

Lemma : closure A = [set | globally A `#` open_nbhs p].

Proof.

by under eq_fun do rewrite -meets_openr meets_globallyl. Qed.

Lemma ( : set T) : A `<=` closure A.

Proof.

by move=> p ??; exists p; split=> //; apply: nbhs_singleton. Qed.

Lemma ( : set T) : closure A = set0 -> A = set0.

Proof.

by move=> A0; apply/seteqP; split => //; rewrite -A0; exact: subset_closure.
Qed.

Lemma ( : set T) : closure (A `&` B) `<=` closure A `&` closure B.

Proof.

by move=> p clABp; split=> ? /clABp [q [[]]]; exists q. Qed.

Definition := [set : T |
forall , nbhs t U -> exists , [/\ y != t, E y & U y]].

Lemma :
limit_point E = [set | globally (E `\ p) `#` nbhs p].

Proof.

under eq_fun do rewrite meets_globallyl; rewrite funeqE => p /=.
apply/eq2_forall => x px; apply/eq_exists => y.
by rewrite propeqE; split => [[/eqP ? ?]|[[? /eqP ?]]]; do 2?split.
Qed.

Lemma :
limit_point E = [set | globally (E `\ p) `#` open_nbhs p].

Proof.

by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed.

Lemma : limit_point E `<=` closure E.

Proof.

by move=> t Et U tU; have [p [? ? ?]] := Et _ tU; exists p. Qed.

Lemma : (~ limit_point A a) =
exists2 : set T, nbhs a X & A `&` X `<=` [set a].

Proof.

rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=.
rewrite not_implyE -forallNE; congr and; apply: eq_forall => t/=.
rewrite and3E not_andE (propext (rwP negP)) negbK implyE orC.
by rewrite -(propext (rwP eqP)).
Qed.

Definition ( : set T) ( : T) :=
x \in A /\ exists2 , nbhs x V & V `&` A = [set x].

Lemma ( : set T) : isolated A `<=` A.

Proof.

by move=> x [/set_mem]. Qed.

Lemma ( : set T) :
[disjoint isolated A & limit_point A].

Proof.

apply/disj_setPS => t [[At [V tV]]] /[swap].
move/(_ _ tV) => [x [xt Ax Vx]].
have /[swap] -> : [set x] `<=` V `&` A by move=> ? ->; split.
move/subset_set1 => [/seteqP[/(_ _ erefl)//]|].
by move=> /seteqP[_ /(_ _ erefl)/=]; apply/eqP; rewrite eq_sym.
Qed.

Lemma ( : set T) :
closure A = isolated A `|` limit_point A.

Proof.

apply/seteqP; split=> [t At0|t [|]].
- rewrite /setU/= -implyNp => /not_andP[tA U /At0[x [Ux Ax]]|+ U tU].
    by exists x; split => //; contra: tA => <-; exact/mem_set.
  move/forall2NP => /(_ U)[//|/seteqP/not_andP[|]].
    by contra => H x [Ux Ax]; apply/eqP/negPn/negP => /H /(_ Ax).
  have [At tUA|At _] := pselect (A t).
    by absurd: tUA => _ ->; split => //; exact: nbhs_singleton.
  have [x [Ax Ux]] := At0 _ tU.
  by exists x; split => //; contra: At => <-.
- by move/isolatedS; exact: subset_closure.
- exact: subset_limit_point.
Qed.

Lemma : closure E = E `|` limit_point E.

Proof.

apply/seteqP; split => [|x]; last first.
by case; [exact: subset_closure|exact: subset_limit_point].
by rewrite closure_isolated_limit_point => x [/isolatedS|]; [left|right].
Qed.

Definition ( : set T) := closure D `<=` D.

Lemma ( : set T) : open D -> closed (~` D).

Proof.

by rewrite openE => Dop p clNDp /Dop /clNDp [? []]. Qed.

Lemma {} ( : set I) ( : I -> set T) :
(forall , D i -> closed (f i)) -> closed (\bigcap_( in D) f i).

Proof.

move=> fcl t clft i Di; have /fcl := Di; apply.
by move=> A /clft [s [/(_ i Di)]]; exists s.
Qed.

Lemma : setI_closed closed.

Proof.

by move=> D E Dcl Ecl p clDEp; split; [apply: Dcl|apply: Ecl];
move=> A /clDEp [q [[]]]; exists q.
Qed.

Lemma : closed setT

Proof.

by []. Qed.

Lemma : closed set0.

Proof.

by move=> ? /(_ setT) [|? []] //; apply: filterT. Qed.

Lemma : closed = [set : set T | forall , ~ (\forall \near p, ~ A x) -> A p].

Proof.

rewrite predeqE => A; split=> Acl p; last first.
by move=> clAp; apply: Acl => /clAp [? []].
rewrite -nbhs_nearE nbhsE => /asboolP.
rewrite asbool_neg => /forallp_asboolPn2 clAp.
apply: Acl => B; rewrite nbhsE => - [C [oC pC]].
have /asboolP := clAp C.
rewrite asbool_or 2!asbool_neg => /orP[/asboolP/not_andP[]//|/existsp_asboolPn [q]].
move/asboolP; rewrite asbool_neg => /imply_asboolPn[+ /contrapT Aq sCB] => /sCB.
by exists q.
Qed.

Lemma ( : set T) : closed D -> open (~` D).

Proof.

by rewrite closedE openE => Dcl t nDt; apply: contrapT => /Dcl. Qed.

Lemma ( : set T) : closed (~` D) = open D.

Proof.

by apply/propext; split=> [/closed_openC|]; [rewrite setCK|exact: open_closedC].
Qed.

Lemma ( : set T) : open (~` D) = closed D.

Proof.

by rewrite -closedC setCK. Qed.

Lemma ( : set T) : closed (closure A).

Proof.

by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed.

End Closed.
#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_isolated_limit_point` instead")]
Notation := __deprecated__closure_limit_point (only parsing).

Lemma { : topologicalType} ( : T -> U) ( : set U) :
{in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D).

Proof.

rewrite !closedE => f_continuous D_cl x /= xDf.
apply: D_cl; apply: contra_not xDf => fxD.
have NDfx : ~ D (f x).
by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact.
by apply: f_continuous fxD; rewrite inE.
Qed.

#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_closed`")]
Notation := preimage_closed (only parsing).

Lemma {} { : topologicalType} {} { : ProperFilter F}
    ( : T -> V) ( : V -> Prop) :
    closed A -> (\forall \near F, A (u_ n)) ->
  forall , u_ @ F --> l -> A l.

Proof.

move=> + FAu_ l u_Fl; apply => B /u_Fl /=; rewrite nbhs_filterE.
by move=> /(filterI FAu_) => /filter_ex[t [Au_t u_Bt]]; exists (u_ t).
Qed.

Arguments closed_cvg {T V F FF u_} _ _ _ _ _.

Lemma ( : topologicalType) ( : S -> T) :
continuous f <-> forall , closed A -> closed (f @^-1` A).

Proof.

rewrite continuousP; split=> ctsf ? ?.
by rewrite -openC preimage_setC; apply: ctsf; rewrite openC.
by rewrite -closedC preimage_setC; apply: ctsf; rewrite closedC.
Qed.

Lemma ( : topologicalType) : setU_closed (@closed T).

Proof.

by move=> E D; rewrite -?openC setCU; exact: openI. Qed.

Lemma { : topologicalType} { : eqType} ( : seq I)
( : I -> set T) : (forall , x \in s -> closed (F x)) ->
closed (\big[setU/set0]_( <- s) F x).

Proof.

move=> scF; rewrite big_seq.
by elim/big_ind : _ => //; [exact: closed0|exact: closedU].
Qed.

#[deprecated(since="mathcomp-analysis 1.17.0", use=bigsetU_closed)]
Notation := bigsetU_closed (only parsing).

Lemma { : topologicalType} { : choiceType} ( : set I)
    ( : I -> set T) :
    finite_set A -> (forall , A i -> closed (F i)) ->
  closed (\bigcup_( in A) F i).

Proof.

move=> finA cF; rewrite -bigsetU_fset_set//; apply: bigsetU_closed => i.
by rewrite in_fset_set// inE; exact: cF.
Qed.

#[deprecated(since="mathcomp-analysis 1.17.0", use=bigcup_closed)]
Notation := bigcup_closed (only parsing).

Section closure_lemmas.
Context { : topologicalType}.
Implicit Types E A B U : set T.

Lemma : A `<=` B -> closure A `<=` closure B.

Proof.

by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed.

#[deprecated(since="mathcomp-analysis 1.16.0", note="Use `closureS` instead.")]
Definition := closureS.

Lemma : closure A = smallest closed A.

Proof.

rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closureS AB).
by apply: smallest_sub; [exact: closed_closure|exact: subset_closure].
Qed.

Lemma : closed E <-> E = closure E.

Proof.

split=> [?|->]; last exact: closed_closure.
by rewrite eqEsubset; split => //; exact: subset_closure.
Qed.

End closure_lemmas.

Section regular_open_closed.
Context { : topologicalType}.

Definition ( : set T) := (closure A)° = A.

Definition ( : set T) := closure (A°) = A.

End regular_open_closed.

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

Lemma : (~` A)° = ~` closure A.

Proof.

rewrite eqEsubset; split=> x; rewrite /closure /interior nbhsE /= -existsNE.
  case=> U ? /disjoints_subset UA; exists U; rewrite not_implyE.
  split; first exact/open_nbhs_nbhs.
  by rewrite setIC UA; apply/set0P; rewrite eqxx.
case=> X; rewrite not_implyE nbhsE=> -[] -[] U xU UX AX0.
exists U => //; apply/(subset_trans UX)/disjoints_subset; rewrite setIC.
exact/eqP/negbNE/negP/set0P.
Qed.

Lemma : closure (~` A) = ~` A°.

Proof.

by apply: setC_inj; rewrite -interiorC !setCK. Qed.

Lemma : A `<=` B -> A° `<=` B°.

Proof.

move=> AB x.
rewrite /interior nbhsE => -[] U oxU UA.
exists U => //; move: UA AB; exact: subset_trans.
Qed.

Lemma : open A <-> interior A = A.

Proof.

by rewrite -(setCK A) openC interiorC closure_id; split => [ <- | /setC_inj->].
Qed.

Lemma : closure [set: T] = [set: T].

Proof.

exact/esym/closure_id/closedT. Qed.

Lemma : closure (@set0 T) = set0.

Proof.

exact/esym/closure_id/closed0. Qed.

Lemma : (@setT T)° = setT.

Proof.

exact/interior_id/openT. Qed.

Lemma : (@set0 T)° = set0.

Proof.

exact/interior_id/open0. Qed.

Lemma : closure (A `|` B) = closure A `|` closure B.

Proof.

by apply: setC_inj; rewrite setCU -!interiorC -interiorI setCU. Qed.

Lemma : A° `|` B° `<=` (A `|` B)°.

Proof.

by apply: subsetC2; rewrite setCU -!closureC setCU; exact: closureI. Qed.

Lemma :
closure A = \bigcap_( in [set | closed C /\ A `<=` C]) x.

Proof.

exact: closureE. Qed.

Lemma : A° = \bigcup_( in [set | open U /\ U `<=` A]) x.

Proof.

apply: setC_inj; rewrite -closureC closureEbigcap setC_bigcup.
rewrite -[RHS](bigcap_image _ setC idfun) /=.
apply: eq_bigcapl; split => X /=.
by rewrite -openC -setCS setCK; exists (~` X)=> //; rewrite setCK.
by case=> Y + <-; rewrite closedC setCS.
Qed.

Lemma :
closure A = \bigcap_( in closed `&` `[A, +oo[) x.

Proof.

rewrite closureEbigcap; apply: eq_bigcapl.
by split => ? /=; rewrite in_itv/= -subsetEset andbT.
Qed.

Lemma : A° = \bigcup_( in open `&` `]-oo, A]) x.

Proof.

apply: setC_inj; rewrite -closureC closureEbigcap_itvcy setC_bigcup.
rewrite -[RHS](bigcap_image _ setC); apply: eq_bigcapl.
apply/seteqP/funext => X.
rewrite -(setCK X) image_inj; first exact: setC_inj.
by rewrite /= !in_itv/= andbT !subsetEset setCS setCK openC.
Qed.

Lemma :
closed B -> A `<=` B -> closure A = \bigcap_( in closed `&` `[A, B]) x.

Proof.

move=> cB; rewrite -subsetEset => AB.
rewrite closureEbigcap_itvcy /bigcap; apply/seteqP.
split => x /= H Y [] cY; rewrite in_itv/= => /andP[] AY YB.
by have:= H Y; apply; split => //; rewrite in_itv/= AY.
apply/(@subIsetl _ _ B)/(H (Y `&` B)); split; first exact: closedI.
rewrite in_itv/=; apply/andP.
by rewrite Order.MeetTheory.lexI Order.MeetTheory.leIr AY AB.
Qed.

Lemma :
open B -> B `<=` A -> A° = \bigcup_( in open `&` `[B, A]) x.

Proof.

rewrite -closedC -subsetCP => cB AB.
apply: setC_inj; rewrite -closureC (closureEbigcap_itvcc cB AB) setC_bigcup.
rewrite -[RHS](bigcap_image _ setC); apply: eq_bigcapl.
apply/seteqP/funext => X.
rewrite -(setCK X) image_inj; first exact: setC_inj.
by rewrite /= !in_itv/= !Order.CTBDistrLatticeTheory.leC setCK openC andbC.
Qed.

Lemma : closed A -> regopen A°.

Proof.

move=> cA; rewrite /regopen eqEsubset; split=> x.
  rewrite /closure [X in X -> _]/interior nbhsE => -[] U oxU UciA.
  rewrite /interior nbhsE /=; exists U => //.
  apply: (subset_trans UciA) => y /= yA.
  apply: cA => B /yA; apply/subset_nonempty; apply: setSI.
  exact: interior_subset.
rewrite {1}/interior nbhsE=> -[] U [] oU Ux UA.
rewrite {1}/interior nbhsE /=; exists U=> //.
have:= UA; rewrite open_subsetE// => /subset_trans; apply.
exact: subset_closure.
Qed.

Lemma : open A -> regclosed (closure A).

Proof.

rewrite /regclosed -(setCK A) openC => cCA.
by rewrite closureC -[in RHS]interior_closed_regopen// !(closureC, interiorC).
Qed.

Lemma : @idempotent_fun (set T) (interior \o closure).

Proof.

move=> ?; exact/interior_closed_regopen/closed_closure. Qed.

Lemma : @idempotent_fun (set T) (closure \o interior).

Proof.

move=> ?; exact/closure_open_regclosed/open_interior. Qed.

End closure_interior_lemmas.
#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `closureC`")]
Notation := closureC (only parsing).

Arguments closureEbigcap_itvcc {T A}.
Arguments interiorEbigcup_itvcc {T A}.

Definition ( : topologicalType) ( : set T) :=
forall ( : set T), O !=set0 -> open O -> O `&` S !=set0.

Lemma ( : topologicalType) ( : set T) : ~ dense S ->
exists , (exists , open_nbhs x O) /\ (O `&` S = set0).

Proof.

rewrite /dense /open_nbhs.
move=> /existsNP[X /not_implyP[[x Xx] /not_implyP[ Ox /forallNP A]]].
by exists X; split; [exists x | rewrite -subset0; apply/A].
Qed.

Lemma ( : topologicalType) ( : set T) :
open A -> dense A -> dense B -> dense (A `&` B).

Proof.

move=> oA dA dB C C0 oC.
have CA0 : C `&` A !=set0 by exact: dA.
suff: (C `&` A) `&` B !=set0 by rewrite setIA.
by apply: dB => //; exact: openI.
Qed.

Lemma { : ptopologicalType} : ~ dense (@set0 R).

Proof.

apply/existsNP; exists setT.
apply/not_implyP; split; first exact/set0P/setT0.
apply/not_implyP; split; first exact: openT.
by rewrite setTI => -[].
Qed.

Section basis.
Context { : topologicalType}.

Definition ( : set_system T) :=
  B `<=` open /\ forall : T, filter_from [set | B U /\ U x] id --> x.

Definition ( : T) ( : set (set T)) :=
  B `<=` nbhs x /\ filter_from [set | B U] id --> x.

Definition ( : set T) := exists ,
  [/\ countable D, D `<=` A &
      forall , A `&` O !=set0 -> open O -> O `&` D !=set0].

Lemma : separable_set set0.

Proof.

by exists set0; split => // U; rewrite set0I => /set0P; rewrite eqxx.
Qed.

Definition := separable_set setT.

Definition := exists2 , countable B & basis B.

Lemma ( : set_system T) : basis B <-> B `<=`open
/\ (forall : set T, open U -> U = \bigcup_( in [set | B W /\ W `<=`U]) V).

Proof.

split=> [[oB bB]|[Bo dec]].
- split=> // U oU.
  apply/seteqP; split => [x Ux/=|]; last by apply: bigcup_sub => V /= [].
  have : nbhs x U by exact: open_nbhs_nbhs.
  by move=> /(bB x U)[V [BV Vx] VU]; exists V.
- split=> // x.
  rewrite /cvg_to nbhsE/= => P [U [/(dec U)->] [A [BA AU] Ax] UP].
  by exists A => // t At; apply: UP; exists A.
Qed.

Lemma : separable = exists : set T, countable A /\ dense A.

Proof.

apply: eq_exists => A.
rewrite [X in [/\ _, _ & X]] (_ : _ = dense A)//.
by under eq_forall do rewrite setTI.
by apply/propext; split=> [|] [].
Qed.

Lemma : second_countable -> separable.

Proof.

have [T0 _|/set0P[x _]] := eqVneq [set: T] set0.
  by rewrite /separable T0; exact: separable_set0.
move=> [B] /(sub_countable (card_le_setD B [set set0])) cB /basisP[BO BB].
have /choice[f nef] : forall , exists , (B `\ set0) U -> U x.
  move=> U.
  have [[BU /eqP/set0P[y Uy]]|/not_andP[|/contrapT]] := pselect ((B `\ set0) U).
  - by exists y.
  - by move=> BU; exists x => -[].
  - by move=> U0; exists x => -[].
exists (f @` (B `\ set0)); split => //.
  exact: (card_le_trans (card_image_le _ _)).
move=> U; rewrite setTI/= => /[swap] /BB -> /bigcup_nonempty[V [BV VU]] V0.
have ? : (B `\ set0) V by split => //; exact/eqP/set0P.
by exists (f V); split; exists V => //; exact: nef.
Qed.

Lemma ( : (set T)^nat) :
(forall , separable_set (A n)) -> separable_set (\bigcup_ A n).

Proof.

move=> /choice[D_ /all_and3[cDx DAx dDx]].
exists (\bigcup_ D_ n); split; [exact: bigcup_countable|exact: subset_bigcup|].
move=> O [x [[n _ Anx] Ox] oO].
have /dDx/(_ oO)[y [Oy Dny]] : A n `&` O !=set0 by exists x.
by exists y; split => //; exact: bigcup_sup Dny.
Qed.

Lemma ( : (set T)^nat) ( : set nat) :
(forall , P n -> separable_set (A n)) ->
separable_set (\bigcup_( in P) A i).

Proof.

rewrite bigcup_mkcond => nPsA; apply: bigcupT_separable => n.
by case: ifPn => [/set_mem/nPsA//|_]; exact: separable_set0.
Qed.

End basis.

Section ClopenSets.
Implicit Type T : topologicalType.

Definition {} ( : set T) := open A /\ closed A.

Lemma {} : setI_closed (@clopen T).

Proof.

by move=> ? ? [] ? ? [] ? ?; split; [exact: openI|exact: closedI]. Qed.

Lemma {} : setU_closed (@clopen T).

Proof.

by move=> ? ? [] ? ? [] ? ?; split; [exact: openU|exact: closedU]. Qed.

Lemma {} ( : set T) : clopen A -> clopen (~`A).

Proof.

by case=> ? ?; split;[exact: closed_openC | exact: open_closedC ]. Qed.

Lemma {} : @clopen T set0.

Proof.

by split; [exact: open0 | exact: closed0]. Qed.

Lemma {} : clopen [set: T].

Proof.

by split; [exact: openT | exact: closedT]. Qed.

Lemma { : topologicalType} ( : T -> U) ( : set U) :
clopen A -> continuous f -> clopen (f @^-1` A).

Proof.

by case=> ? ?; split; [ exact: open_comp | exact: preimage_closed]. Qed.

End ClopenSets.
#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_clopen`")]
Notation := preimage_clopen (only parsing).

. (f : X -> Y):= {
  continuous_fun : continuous f
}.

( )
. := {
   of @isContinuous X Y f
}.

#[deprecated(since="mathcomp-analysis 1.17.0",
             note="use `continuous_fun` instead")]
Notation := (continuous_fun) (only parsing).

. :=
  gen_eqMixin (continuousType X Y).
. :=
  gen_choiceMixin (continuousType X Y).

Lemma { : nbhsType} ( : continuousType X Y) :
  f = g <-> f =1 g.

Proof.

case: f g => [f [[ffun]]] [g [[gfun]]]/=; split=> [[->//]|/funext eqfg].
rewrite eqfg in ffun *; congr {| Continuous.sort := _; Continuous.class := {|
Continuous.topology_structure_isContinuous_mixin :=
{|isContinuous.continuous_fun := _|}|}|}.
exact: Prop_irrelevance.
Qed.

Definition { : nbhsType} ( : X -> Y) ( : continuous f) := f.

. (f: X -> Y) (f_cts : continuous f) :=
@isContinuous.Build X Y (mkcts f_cts) f_cts.

Section continuous_comp.
Context { : topologicalType}
( : continuousType X Y) ( : continuousType Y Z).

#[local] Lemma : continuous (g \o f).

Proof.

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

..Build X Z (g \o f) cts_fun_comp.

End continuous_comp.

Section continuous_id.
Context { : topologicalType}.

..Build X X (@idfun X) id_continuous.

End continuous_id.

Section continuous_const.
Context { : topologicalType} ( : Y).

#[local] Lemma : continuous (@cst X Y y).

Proof.

by move=> x; exact: cvg_cst. Qed.

..Build X Y (cst y) cts_const.

End continuous_const.

Files

Module mathcomp.analysis.topology_theory.topology_structure