Files

  • mathcomp

    • 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 {
    ISource code
     : choiceType} {
    XSource code
     : I -> topologicalType}.

    Definition
    sigT_nbhs

    set_nbhs : forall {T : topologicalType}, set T -> set (set T) set_nbhs is not universe polymorphic Arguments set_nbhs {T} A%_classical_set_scope _ set_nbhs is transparent Expands to: Constant mathcomp.analysis.topology_theory.separation_axioms.set_nbhs Declared in library mathcomp.analysis.topology_theory.separation_axioms, line 66, characters 11-19

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

    Lemma
    sigT_nbhsEUsed by
    • mathcomp.analysis.topology_theory.separation_axioms
    Source code
     (
    iSource code
     : I) (
    xSource code
     : X i) :
      sigT_nbhs (existT _ i x) = (existT _ _) @ (nbhs x).
    Proof.
    by done. Qed.

    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code
    hasNbhsSource code
    .Build {
    iSource code
     & X i} sigT_nbhs.

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

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

    Local Lemma
    sigT_nbhs_nbhsSource code
    xSource code
    ASource 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.

    HBSource code
    .
    instanceSource code
    DefinitionSource code
    _Source code
    :=Source code
    Nbhs_isNbhsTopologicalSource code
    .Build {
    iSource code
     & X i}
      sigT_nbhs_proper sigT_nbhs_singleton sigT_nbhs_nbhs.

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

    Lemma
    existT_open_mapUsed by
    • mathcomp.analysis.homotopy_theory.wedge_sigT
    Source code
     (
    iSource code
     : I) (
    ASource 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_nbhsUsed by
    • mathcomp.analysis.topology_theory.separation_axioms
    Source code
     (
    iSource code
     : I) (
    xSource code
     : X i) (
    USource code
     : set (X i)) :
      nbhs x U -> nbhs (existT _ i x) (existT _ i @` U).
    Proof.
    exact/filterS/preimage_image. Qed.

    Lemma
    sigT_openPUsed by
    • mathcomp.analysis.homotopy_theory.wedge_sigT
    Source code
     (
    USource code
     : set {
    iSource code
     & X i}) :
      open U <-> forall
    iSource 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_continuousUsed by
    • mathcomp.analysis.homotopy_theory.wedge_sigT
    Source code
     {
    ZSource code
     : topologicalType} (
    fSource code
     : forall
    iSource code
    , X i -> Z) :
      (forall
    iSource code
    , continuous (f i)) -> continuous (sigT_fun f).
    Proof.
    by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed.

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

    Lemma
    sigT_compactSource code
     : finite_set [set: I] -> (forall
    iSource code
    , compact [set: X i]) ->
      compact [set: {
    iSource 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

    Source

    Uses
    Used By