diff --git a/theories/cantor.v b/theories/cantor.v index c1af3b0b84..fdcbaba775 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -43,114 +43,6 @@ Qed. Lemma cantor_space_hausdorff : hausdorff_space cantor_space. Proof. apply: hausdorff_product => ?; exact: discrete_hausdorff. Qed. -Definition common_prefix (n : nat) (x y : cantor_space) := - (forall i, i < n -> x i == y i). - -Definition pull (x : cantor_space) : cantor_space := fun n => x (S n). - -Lemma common_prefixS (n : nat) (x y : cantor_space) : - common_prefix n.+1 x y <-> x 0 == y 0 /\ common_prefix n (pull x) (pull y). -Proof. -split; last by case=> ?? []. -by (move=> cmn; split; first exact: cmn) => i ?; apply: cmn. -Qed. - -Lemma empty_prefix (x : cantor_space) : common_prefix 0 x = setT . -Proof. by rewrite eqEsubset; split. Qed. - -Lemma prefix_of_prefix (x : cantor_space) (n : nat) : - common_prefix n x x. -Proof. by move=> ?. Qed. - -Lemma fixed_prefixW (x : cantor_space) (i j : nat) : - i < j -> - common_prefix j x `<=` common_prefix i x. -Proof. by move=> ij y + q ?; apply; apply: (ltn_trans _ ij). Qed. - -Lemma prefix_cvg (x : cantor_space) : - filter_from [set: nat] (common_prefix^~ x) --> x. -Proof. -have ? : Filter (filter_from [set: nat] (common_prefix^~ x)). - apply: filter_from_filter; first by exists 0. - move=> i j _ _; exists (i.+1 + j.+1) => //; rewrite -[x in x `<=` _]setIid. - by apply: setISS; apply: fixed_prefixW; [exact: ltn_addr| exact: ltn_addl]. -apply/cvg_sup => n; apply/cvg_image; first by (rewrite eqEsubset; split). -move=> W /=; rewrite /nbhs /= => /principal_filterP. -have [] := (@subset_set2 _ W true false). -- by rewrite -bool2E; exact: subsetT. -- by move ->. -- move => -> <-; exists (common_prefix (n.+1) x); first by exists (n.+1). - rewrite eqEsubset; split => y; first by case=> z P <-; apply/sym_equal/eqP/P. - by move=> ->; exists x => //=; exact: (prefix_of_prefix x (n.+1)). -- move => -> <-; exists (common_prefix (n.+1) x); first by exists (n.+1). - rewrite eqEsubset; split => y; first by case=> z P <-; apply/sym_equal/eqP/P. - by move=> ->; exists x => //=; exact: (prefix_of_prefix x (n.+1)). -- rewrite -bool2E => ->; exists setT; last by rewrite eqEsubset; split. - exact: filterT. -Qed. - -Lemma nbhs_prefix (x : cantor_space) (W : set cantor_space) : - nbhs x W -> exists n, common_prefix n x `<=` W. -Proof. by move=> /prefix_cvg => /=; case=> n _ ?; exists n. Qed. - -Lemma pull_projection_preimage (n : nat) (b : bool) : - pull @^-1` (proj n @^-1` [set b]) = proj (n.+1) @^-1` [set b]. -Proof. by rewrite eqEsubset; split=> x /=; rewrite /proj /pull /=. Qed. - -Lemma continuous_pull : continuous pull. -move=> x; apply/ cvg_sup; first by apply: fmap_filter; case: (nbhs_filter x). -move=> n; apply/cvg_image; first by apply: fmap_filter; case: (nbhs_filter x). - by rewrite eqEsubset; split=> u //= _; exists (fun=> u). -move=> W. -have Q: nbhs [set[set f n | f in A] | A in pull x @[x --> x]] [set pull x n]. - exists (proj n @^-1` [set (pull x n)]); first last. - rewrite eqEsubset; split => u //=; first by by case=> ? <- <-. - move->; exists (pull x) => //=. - apply: open_nbhs_nbhs; split. - rewrite pull_projection_preimage; apply: open_comp; last exact: discrete_open. - by move=> + _; apply: proj_continuous. - done. -have [] := (@subset_set2 _ W true false). -- by rewrite -bool2E; exact: subsetT. -- by move=> ->; rewrite /nbhs /= => /principal_filterP. -- by move -> => /= /nbhs_singleton <-; exact Q. -- by move -> => /= /nbhs_singleton <-; exact Q. -- rewrite -bool2E => -> _; exists setT; last by rewrite eqEsubset; split. - by rewrite /= preimage_setT; exact: filterT. -Qed. - -Lemma open_prefix (x : cantor_space) (n : nat) : - open (common_prefix n x). -Proof. -move: x; elim: n; first by move=>?; rewrite empty_prefix; exact: openT. -move=> n IH x; rewrite openE=> z /common_prefixS [/eqP x0z0] cmn; near=> y. -apply/common_prefixS; split. - apply/eqP; rewrite x0z0; apply: sym_equal; near: y; near_simpl. - have : open_nbhs (z : cantor_space) (proj 0 @^-1` [set (z 0)]). - (split; last by []); apply: open_comp => //=; last exact: discrete_open. - by move=> + _; exact: proj_continuous. - by rewrite open_nbhsE => [[_]]. -by near: y; by move: (IH (pull x)); rewrite openE => /(_ _ cmn)/continuous_pull. -Unshelve. all: end_near. Qed. - -Lemma closed_fixed (x : cantor_space) (n : nat) : closed (common_prefix n x). -Proof. -move: x; elim: n; first by move=> ?; rewrite empty_prefix; exact: closedT. -move=> n IH x. -pose B1 : set cantor_space := pull @^-1` common_prefix n (pull x). -pose B2 : set cantor_space := proj 0 @^-1` [set x 0]. -suff <- : B1 `&` B2 = common_prefix n.+1 x. - apply: closedI; apply: closed_comp. - - move=> + _; exact: continuous_pull. - - exact: IH. - - move=> + _; exact: proj_continuous. - - apply: compact_closed => //=; last exact: compact_set1. - exact: discrete_hausdorff. -rewrite eqEsubset; split => y /=; rewrite common_prefixS; case=> P Q. -(split => //; first (by apply/eqP)). -by move/eqP: P. -Qed. - Section perfect_sets. Implicit Types (T : topologicalType). @@ -239,25 +131,6 @@ End clopen. Definition totally_disconnected (T : topologicalType) := forall (x y : T), x != y -> exists A, A x /\ ~ A y /\ clopen A. -Lemma cantor_totally_disconnected : totally_disconnected cantor_space. -Proof. -move=> x y; have := cantor_space_hausdorff; rewrite open_hausdorff => chsdf. -move=> /chsdf [[A B /=]]; rewrite ?inE => [[Ax By] [] + oB AB0]. -rewrite {1}openE => /(_ _ Ax) /nbhs_prefix [N] pfxNsubA. -exists (common_prefix N x); split => //; split. - by move=> /pfxNsubA Ay; suff : (A `&` B) y by rewrite AB0. -split; [apply: open_prefix | apply: closed_fixed]. -Qed. - -Lemma cantor_perfect : perfect_set [set: cantor_space]. -Proof. -split; [exact: closedT|]; rewrite eqEsubset; split => x // _. -move=> A /nbhs_prefix [N] pfxNsubA. -exists (fun n => if N < n then ~~ x n else x n); split => //. -- apply/eqP; rewrite funeqE; apply/existsNP; exists N.+1. - by rewrite ltnSn; exact: Bool.no_fixpoint_negb. -by apply: pfxNsubA => i /ltnW/leq_gtF ->. -Qed. Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) : clopen A -> continuous f -> clopen (f @^-1` A). @@ -282,12 +155,22 @@ move=> dsct x y /eqP xneqy; exists [set x]; split; [|split] => //. by split => //; [exact: discrete_open | exact: discrete_closed]. Qed. +Lemma cantor_totally_disconnected : totally_disconnected cantor_space. +Proof. +by apply: totally_disconnected_prod => _; apply: totally_disconnected_discrete. +Qed. + +Lemma cantor_perfect : perfect_set [set: cantor_space]. +Proof. +by apply: perfect_diagonal => _; exists (true, false). +Qed. + Definition countable_basis (T : topologicalType) := exists B, [/\ countable B, forall A, B A -> open A & forall (x:T) V, nbhs x V -> exists A, B A /\ nbhs x A /\ A `<=` V]. -Definition cantor_like {R} (T : pseudoMetricType R) := +Definition cantor_like (T : topologicalType) := [/\ perfect_set [set: T], compact [set: T], hausdorff_space T @@ -307,11 +190,6 @@ move=> oA /closed_openC oAc; apply/continuousP; rewrite bool_predE; split => _. - rewrite -bool2E preimage_setT; exact: openT. Qed. -Definition separates_points_from_closed {I : Type} {T : topologicalType} - {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := - forall (U : set T) x, - closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). - Lemma discrete_closed {T : topologicalType} (dsc : discrete_space T) A : @closed T A. Proof. rewrite -openC; exact: discrete_open. Qed. @@ -349,7 +227,7 @@ move=> /( _ _ _ (fun C y => ~ C y) (powerset_filter_from_filter PF)); case. by move=> D [] DF Dsub [C] DC /(_ _ DC) /subsetC2/filterS; apply; exact: DF. Qed. -Lemma clopen_countable {T : topologicalType} : +Lemma clopen_countable {T : topologicalType}: compact [set: T] -> countable_basis T -> countable (@clopen T). @@ -731,8 +609,7 @@ Qed. End TreeStructure. -Lemma cantor_like_cantor_space {R : realType}: - cantor_like (@cantor_psuedoMetric R). +Lemma cantor_like_cantor_space: cantor_like (cantor_space). Proof. split. - by apply: perfect_diagonal => //= _; exists (true, false).