Files

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
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