From 729dad75f632636cee9a4133837504e826af2fb3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 28 Oct 2024 10:08:03 +0900 Subject: [PATCH] wo destruct --- theories/separation_axioms.v | 31 +++++------ theories/topology_theory/sum_topology.v | 68 +++++++++++-------------- 2 files changed, 45 insertions(+), 54 deletions(-) diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 71e9b2ba6..281532c4b 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1129,22 +1129,19 @@ End perfect_sets. Section sum_separations. Context {I : choiceType} {X : I -> topologicalType}. -Lemma sum_hausdorff : +Lemma sum_hausdorff : (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}. Proof. -move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= ?sum_nbhsE /= => cl. -have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]). -- by apply: existT_nbhs; exact: filterT. -- by apply: existT_nbhs; exact: filterT. -(* TODO: get rid of dependent destruct *) -move=> p [/= [? _] <- [ ? _]] [] E; destruct E => _. -congr( _ _); apply: hX => U V Ux Vy. -have [] := cl (existT X j @` U) (existT X j @` V). -- exact: existT_nbhs. -- exact: existT_nbhs. -move=> z [/= [l] ?] <- [r] Vr lr; exists l; split => //. -move: Vr; have -> // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr. -by move=> a b; case: (pselect (a = b)) => ?; [left | right]. -Qed. - -End sum_separations. \ No newline at end of file +move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sum_nbhsE /= => cl. +have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]); + [by apply: existT_nbhs; exact: filterT..|]. +move=> p [/= [_ _ <-] [_ _ [ji]]] _. +rewrite {}ji {j} in x y cl *. +congr existT; apply: hX => U V Ux Vy. +have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. +move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. +rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr. +by move=> a b; exact: pselect. +Qed. + +End sum_separations. diff --git a/theories/topology_theory/sum_topology.v b/theories/topology_theory/sum_topology.v index 986b7e78f..d7faf31cf 100644 --- a/theories/topology_theory/sum_topology.v +++ b/theories/topology_theory/sum_topology.v @@ -19,10 +19,10 @@ Local Open Scope ring_scope. Section sum_topology. Context {I : choiceType} {X : I -> topologicalType}. -Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := - (existT _ _) @ (nbhs (projT2 x)). +Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := + existT _ _ @ nbhs (projT2 x). -Lemma sum_nbhsE (i : I) (x : X i) : +Lemma sum_nbhsE (i : I) (x : X i) : sum_nbhs (existT _ i x) = (existT _ _) @ (nbhs x). Proof. by done. Qed. @@ -32,62 +32,56 @@ Local Lemma sum_nbhs_proper x : ProperFilter (sum_nbhs x). Proof. by case: x => i xi; exact: fmap_proper_filter. Qed. Local Lemma sum_nbhs_singleton x A : sum_nbhs x A -> A x. -Proof. by case: x => ? ? /=; apply: nbhs_singleton. Qed. +Proof. by case: x => ? ? /=; exact: nbhs_singleton. Qed. Local Lemma sum_nbhs_nbhs x A: sum_nbhs x A -> sum_nbhs x (sum_nbhs^~ A). -Proof. -case: x => i zi /=. - rewrite sum_nbhsE /= nbhsE /=; case => W [oW Wz WlA]. - exists W; first by split. - move=> x /= ?; move/filterS: WlA; apply. - by apply: open_nbhs_nbhs. +Proof. +case: x => i Xi /=. +rewrite sum_nbhsE /= nbhsE /= => -[W [oW Wz WlA]]. +by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs. Qed. HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i} sum_nbhs_proper sum_nbhs_singleton sum_nbhs_nbhs. -Lemma existT_continuous (i : I) : continuous (existT X i). +Lemma existT_continuous (i : I) : continuous (existT X i). Proof. by move=> ? ?. Qed. -Lemma existT_open_map (i : I) (A : set (X i)): open A -> open (existT X i @` A). -Proof. -move=> oA; rewrite openE /interior /= => ?. -case=> x Ax <-; rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. +Lemma existT_open_map (i : I) (A : set (X i)) : open A -> open (existT X i @` A). +Proof. +move=> oA; rewrite openE /interior /= => iXi [x Ax <-]. +rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. move: oA; rewrite openE => /(_ _ Ax); apply: filterS. -by move=> z => Az; exists z. +by move=> z Az; exists z. Qed. -Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : +Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : nbhs x U -> nbhs (existT _ i x) (existT _ i @` U). -Proof. by move/filterS; apply; exact: preimage_image. Qed. +Proof. exact/filterS/preimage_image. Qed. -Lemma sum_openP (U : set {i & X i}) : - open U <-> (forall i, open (existT _ i@^-1` U)). +Lemma sum_openP (U : set {i & X i}) : + open U <-> forall i, open (existT _ i @^-1` U). Proof. -split => ?. - by move=> i; apply: open_comp=> //; move=> y _; exact: existT_continuous. -rewrite openE /interior; case=> i x Uxi. -rewrite /nbhs /= sum_nbhsE; apply: open_nbhs_nbhs; split => //. +split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous. +rewrite openE => -[i x Uxi]. +by rewrite /interior /nbhs/= sum_nbhsE; exact: open_nbhs_nbhs. Qed. -Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : +Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : (forall i, continuous (f i)) -> continuous (sum_fun f). Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed. -Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: (X i)]). -Proof. -by rewrite eqEsubset; split; case=> i x //=; first by move=> _; exists i. -Qed. +Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]). +Proof. by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed. -Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> - compact [set: {i&X i}]. +Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> + compact [set: {i & X i}]. Proof. -move=> fsetI cptX. -rewrite sum_setUE -fsbig_setU //; apply: big_ind. -- exact: compact0. -- by move=> ? ? ? ?; exact: compactU. -move=> i _; apply: continuous_compact; last exact: cptX. -by apply: continuous_subspaceT; exact: existT_continuous. +move=> fsetI cptX; rewrite sum_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 sum_topology.