Skip to content

Commit

Permalink
expanding opc acronym
Browse files Browse the repository at this point in the history
  • Loading branch information
zstone1 committed Oct 23, 2024
1 parent 62d5633 commit 2f916d2
Show file tree
Hide file tree
Showing 4 changed files with 51 additions and 29 deletions.
25 changes: 18 additions & 7 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -170,21 +170,32 @@
+ lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
- in file `normedtype.v`,
+ new definition `type` (in module `completely_regular_uniformity`)
+ new lemmas `normal_completely_regular`, `completely_reg_opc`,
`nbhs_opc_weakE`, `locally_compact_completely_regular`, and
+ new lemmas `normal_completely_regular`, and
`locally_compact_completely_regular`.
+ new definition `type`.
+ new lemmas `normal_completely_regular`,
`one_point_compactification_completely_reg`,
`nbhs_one_point_compactification_weakE`,
`locally_compact_completely_regular`, and
`completely_regular_regular`.

- in file `topology.v`,
+ new definitions `one_point_compactification`, and `one_point_nbhs`.
+ new lemmas `compact_normal_local`, `compact_normal`, `opc_compact`,
`opc_some_nbhs`, `opc_some_continuous`, `opc_open_some`,
`opc_weak_topology`, and `opc_hausdorff`.
+ new lemmas `compact_normal_local`, and `compact_normal`.
+ new lemmas `one_point_compactification_compact`,
`one_point_compactification_some_nbhs`,
`one_point_compactification_some_continuous`,
`one_point_compactification_open_some`,
`one_point_compactification_weak_topology`, and
`one_point_compactification_hausdorff`.
- in file `separation_axioms.v`
+ new lemmas `compact_normal_local` and `compact_normal`.

### Changed

- in file `normedtype.v`,
- in file `normedtype.v`,
changed `completely_regular_space` to depend on uniform separators
which removes the dependency on R. The old formulation can be
which removes the dependency on R. The old formulation can be
recovered easily with uniform_separatorP.

### Renamed
Expand Down
22 changes: 13 additions & 9 deletions theories/normedtype.v
Original file line number Diff line number Diff line change
Expand Up @@ -3807,19 +3807,23 @@ Hypothesis hsdf : hausdorff_space X.

Let opc := @one_point_compactification X.

Lemma completely_reg_opc : completely_regular_space opc.
Lemma one_point_compactification_completely_reg :
completely_regular_space opc.
Proof.
apply: normal_completely_regular.
by apply: compact_normal; [exact: opc_hausdorff|exact: opc_compact].
by apply: hausdorff_accessible; exact: opc_hausdorff.
apply: normal_completely_regular.
apply: compact_normal.
exact: one_point_compactification_hausdorff.
exact: one_point_compactification_compact.
by apply: hausdorff_accessible; exact: one_point_compactification_hausdorff.
Qed.
#[local]
HB.instance Definition _ := Uniform.copy opc
(completely_regular_uniformity.type completely_reg_opc).
HB.instance Definition _ := Uniform.copy opc
(completely_regular_uniformity.type
one_point_compactification_completely_reg).

Let X' := @weak_topology X opc Some.
Lemma nbhs_opc_weakE : @nbhs X X = nbhs_ (@entourage X').
Proof. by rewrite nbhs_entourageE opc_weak_topology. Qed.
Lemma nbhs_one_point_compactification_weakE : @nbhs X X = nbhs_ (@entourage X').
Proof. by rewrite nbhs_entourageE one_point_compactification_weak_topology. Qed.

#[local, non_forgetful_inheritance]
HB.instance Definition _ := @Nbhs_isUniform.Build
Expand All @@ -3829,7 +3833,7 @@ HB.instance Definition _ := @Nbhs_isUniform.Build
(@entourage_diagonal_subproof X')
(@entourage_inv X')
(@entourage_split_ex X')
nbhs_opc_weakE.
nbhs_one_point_compactification_weakE.

Lemma locally_compact_completely_regular : completely_regular_space X.
Proof. exact: uniform_completely_regular. Qed.
Expand Down
10 changes: 6 additions & 4 deletions theories/separation_axioms.v
Original file line number Diff line number Diff line change
Expand Up @@ -257,8 +257,10 @@ Import numFieldTopology.Exports.
Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
Proof. exact: order_hausdorff. Qed.

Lemma opc_hausdorff {X : topologicalType} : locally_compact [set: X] ->
hausdorff_space X -> hausdorff_space (one_point_compactification X).
Lemma one_point_compactification_hausdorff {X : topologicalType} :
locally_compact [set: X] ->
hausdorff_space X ->
hausdorff_space (one_point_compactification X).
Proof.
move=> lcpt hsdfX [x|] [y|] //=.
- move=> clxy; congr Some; apply: hsdfX => U V Ux Vy.
Expand All @@ -269,12 +271,12 @@ move=> lcpt hsdfX [x|] [y|] //=.
by exists p.
- have [U] := lcpt x I; rewrite withinET => Ux [] cU clU.
case/(_ (Some @` U) (Some @` (~` U) `|` [set None])).
+ exact: opc_some_nbhs.
+ exact: one_point_compactification_some_nbhs.
+ by exists U.
+ by move=> [?|] [][]// z /[swap]/Some_inj <- ? []//= [? /[swap]/Some_inj ->].
- have [U] := lcpt y I; rewrite withinET => Uy [] cU clU.
case/(_ (Some @` (~` U) `|` [set None]) (Some @` U) ); first by exists U.
exact: opc_some_nbhs.
exact: one_point_compactification_some_nbhs.
case => [?|] [][]//= + [] ? // /[swap] /Some_inj ->.
by case => ? /[swap] /Some_inj <-.
Qed.
Expand Down
23 changes: 14 additions & 9 deletions theories/topology.v
Original file line number Diff line number Diff line change
Expand Up @@ -103,8 +103,10 @@ Require Import reals signed.
(* is both open and closed in A is A *)
(* separated A B == the two sets A and B are separated *)
(* connected_component x == the connected component of point x *)
(* one_point_compactification X == the one point compactification of X *)
(* one_point_compactification X == the one-point compactification of X *)
(* built on the type (option X). *)
(* one_point_nbhs X == the neighborhoods of the one-point *)
(* compactification. *)
(* ``` *)
(* *)
(* ### Uniform spaces *)
Expand Down Expand Up @@ -4540,7 +4542,7 @@ HB.instance Definition _ := hasNbhs.Build opc one_point_nbhs.
HB.instance Definition _ := @Nbhs_isNbhsTopological.Build opc
one_point_filter one_point_singleton one_point_nbhs_nbhs.

Lemma opc_compact : compact [set: opc].
Lemma one_point_compactification_compact : compact [set: opc].
Proof.
apply/compact_near_coveringP => ? F /= P FF FT.
have [//| [U i [[W /= [cptW cW WU nfI UIP]]]]] := FT None.
Expand All @@ -4558,29 +4560,32 @@ move=> ?; apply: (UIP (Some z,j)); split => //=.
exact: (near nfI _).
Unshelve. all: by end_near. Qed.

Lemma opc_some_nbhs (x : X) (U : set X) :
Lemma one_point_compactification_some_nbhs (x : X) (U : set X) :
nbhs x U -> @nbhs _ opc (Some x) (Some @` U).
Proof.
by rewrite {2}/nbhs /= nbhs_simpl /= => /filterS; apply; exact: preimage_image.
Qed.

Lemma opc_some_continuous : continuous (Some : X -> opc).
Lemma one_point_compactification_some_continuous : continuous (Some : X -> opc).
Proof. by move=> x U. Qed.

Lemma opc_open_some (U : set X) : open U -> @open opc (Some @` U).
Lemma one_point_compactification_open_some (U : set X) :
open U -> @open opc (Some @` U).
Proof.
rewrite ?openE /= => Uo ? /= [x /[swap] <- Ux] /=.
by apply: opc_some_nbhs; exact: Uo.
by apply: one_point_compactification_some_nbhs; exact: Uo.
Qed.

Lemma opc_weak_topology : @nbhs _ (@weak_topology X opc Some) = @nbhs _ X.
Lemma one_point_compactification_weak_topology :
@nbhs _ (@weak_topology X opc Some) = @nbhs _ X.
Proof.
rewrite funeq2E=> x U; apply/propeqP; split;
rewrite /(@nbhs _ (weak_topology _)) /=.
case => V [[/= W] oW <- /= Ws] /filterS; apply; apply: opc_some_continuous.
case => V [[/= W] oW <- /= Ws] /filterS; apply;
apply: one_point_compactification_some_continuous.
exact: oW.
rewrite nbhsE; case => V [? ? ?]; exists V; split => //.
exists (Some @` V); first exact: opc_open_some.
exists (Some @` V); first exact: one_point_compactification_open_some.
rewrite eqEsubset; split => z /=; first by case=> ? /[swap] /Some_inj ->.
by move=> ?; exists z.
Qed.
Expand Down

0 comments on commit 2f916d2

Please sign in to comment.