Files

  • mathcomp

    • Top source

    Module mathcomp.analysis.topology_theory.sigT_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 compact subspace_topology.

    # sigT topology This file equips the type {i & X i} with its standard topology ``` sigT_nbhs x == the neighborhoods of the standard topology on the type {i & X i} ```

    Unset SsrOldRewriteGoalsOrder.

    Local Open Scope classical_set_scope.
    Local Open Scope ring_scope.

    Section sigT_topology.
    Context {
    I
    Source code
     : choiceType} {
    X
    Source code
     : I -> topologicalType}.

    Definition
    sigT_nbhs

    sigT_nbhs : forall {I : choiceType} {X : I -> topology_structure.Topological.type}, {i : I & topology_structure.Topological.sort (X i)} -> set_system {i : I & topology_structure.Topological.sort (X i)} sigT_nbhs is not universe polymorphic Arguments sigT_nbhs {I} {X}%_function_scope x _ sigT_nbhs is transparent Expands to: Constant mathcomp.analysis.topology_theory.sigT_topology.sigT_nbhs Declared in library mathcomp.analysis.topology_theory.sigT_topology, line 26, characters 11-20

    Source code
     (
    x
    Source code
     : {
    i
    Source code
     & X i}) : set_system {
    i
    Source code
     & X i} :=
      existT _ _ @ nbhs (projT2 x).

    Lemma
    sigT_nbhsE
    Source code
     (
    i
    Source code
     : I) (
    x
    Source code
     : X i) :
      sigT_nbhs (existT _ i x) = (existT _ _) @ (nbhs x).
    Proof.
    by done. Qed.

    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    hasNbhs
    Source code
    .Build {
    i
    Source code
     & X i} sigT_nbhs.

    Local Lemma
    sigT_nbhs_proper
    Source code
    x
    Source code
     : ProperFilter (sigT_nbhs x).
    Proof.
    by case: x => i xi; exact: fmap_proper_filter. Qed.

    Local Lemma
    sigT_nbhs_singleton
    Source code
    x
    Source code
    A
    Source code
     : sigT_nbhs x A -> A x.
    Proof.
    by case: x => ? ? /=; exact: nbhs_singleton. Qed.

    Local Lemma
    sigT_nbhs_nbhs
    Source code
    x
    Source code
    A
    Source code
    : sigT_nbhs x A -> sigT_nbhs x (sigT_nbhs^~ A).
    Proof.
    case: x => i Xi /=.
    rewrite sigT_nbhsE /= nbhsE /= => -[W [oW Wz WlA]].
    by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs.
    Qed.

    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    Nbhs_isNbhsTopological
    Source code
    .Build {
    i
    Source code
     & X i}
      sigT_nbhs_proper sigT_nbhs_singleton sigT_nbhs_nbhs.

    Lemma
    existT_continuous
    Source code
     (
    i
    Source code
     : I) : continuous (existT X i).
    Proof.
    by move=> ? ?. Qed.

    Lemma
    existT_open_map
    Source code
     (
    i
    Source code
     : I) (
    A
    Source code
     : set (X i)) : open A -> open (existT X i @` A).
    Proof.
    move=> oA; rewrite openE /interior /= => iXi [x Ax <-].
    rewrite /nbhs /= sigT_nbhsE /= nbhs_simpl /=.
    move: oA; rewrite openE => /(_ _ Ax); apply: filterS.
    by move=> z Az; exists z.
    Qed.

    Lemma
    existT_nbhs
    Source code
     (
    i
    Source code
     : I) (
    x
    Source code
     : X i) (
    U
    Source code
     : set (X i)) :
      nbhs x U -> nbhs (existT _ i x) (existT _ i @` U).
    Proof.
    exact/filterS/preimage_image. Qed.

    Lemma
    sigT_openP
    Source code
     (
    U
    Source code
     : set {
    i
    Source code
     & X i}) :
      open U <-> forall
    i
    Source code
    , open (existT _ i @^-1` U).
    Proof.
    split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous.
    rewrite openE => -[i x Uxi].
    by rewrite /interior /nbhs/= sigT_nbhsE; exact: open_nbhs_nbhs.
    Qed.

    Lemma
    sigT_continuous
    Source code
     {
    Z
    Source code
     : topologicalType} (
    f
    Source code
     : forall
    i
    Source code
    , X i -> Z) :
      (forall
    i
    Source code
    , continuous (f i)) -> continuous (sigT_fun f).
    Proof.
    by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed.

    Lemma
    sigT_setUE
    Source code
     : [set: {
    i
    Source code
     & X i}] = \bigcup_
    i
    Source code
     (existT _ i @` [set: X i]).
    Proof.
    by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed.

    Lemma
    sigT_compact
    Source code
     : finite_set [set: I] -> (forall
    i
    Source code
    , compact [set: X i]) ->
      compact [set: {
    i
    Source code
     & X i}].
    Proof.
    move=> fsetI cptX; rewrite sigT_setUE -fsbig_setU//.
    apply: big_rec; first exact: compact0.
    move=> i ? _ cptx; apply: compactU => //.
    apply: continuous_compact; last exact: cptX.
    exact/continuous_subspaceT/existT_continuous.
    Qed.

    End sigT_topology.
    Generated by rocqnavi