Skip to content

define joins of POrder and Topological #1810

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
affeldt-aist merged 1 commit into from
Dec 27, 2025
Merged

define joins of POrder and Topological #1810

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 21 additions & 6 deletions theories/topology_theory/order_topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,21 @@ Unset Printing Implicit Defensive.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HB.structure Definition POrderedNbhs d :=
{ T of Nbhs T & Order.isPOrder d T }.

HB.structure Definition POrderedTopological d :=
{ T of Topological T & Order.isPOrder d T }.

HB.structure Definition POrderedUniform d :=
{T of Uniform T & Order.isPOrder d T}.

HB.structure Definition POrderedPseudoMetric d (R : numDomainType) :=
{T of PseudoMetric R T & Order.isPOrder d T}.

HB.structure Definition POrderedPointedTopological d :=
{T of PointedTopological T & Order.isPOrder d T}.

(** TODO: generalize this to a preOrder once that's available *)
HB.mixin Record Order_isNbhs d (T : Type) of Nbhs T & Order.Total d T := {
(** Note that just the intervals `]a, b[ doesn't work when the order has a
Expand Down Expand Up @@ -53,21 +68,21 @@ Local Open Scope classical_set_scope.
Context {d} {T : orderTopologicalType d}.
Implicit Types x y : T.

Lemma rray_open x : open `]x, +oo[.
Lemma rray_open x : @open T `]x, +oo[.
Proof.
rewrite openE /interior => z xoz; rewrite itv_nbhsE.
by exists `]x, +oo[%O => //; split => //; left.
Qed.
Hint Resolve rray_open : core.

Lemma lray_open x : open `]-oo, x[.
Lemma lray_open x : @open T `]-oo, x[.
Proof.
rewrite openE /interior => z xoz; rewrite itv_nbhsE.
by exists (`]-oo, x[)%O => //; split => //; left.
Qed.
Hint Resolve lray_open : core.

Lemma itv_open x y : open `]x, y[.
Lemma itv_open x y : @open T `]x, y[.
Proof. by rewrite set_itv_splitI /=; apply: openI. Qed.
Hint Resolve itv_open : core.

Expand All @@ -77,15 +92,15 @@ case: i; rewrite /itv_open_ends => [[[]t1|[]]] [[]t2|[]] []? => //.
by rewrite set_itvE; exact: openT.
Qed.

Lemma rray_closed x : closed `[x, +oo[.
Lemma rray_closed x : @closed T `[x, +oo[.
Proof. by rewrite -setCitvl closedC. Qed.
Hint Resolve rray_closed : core.

Lemma lray_closed x : closed `]-oo, x].
Lemma lray_closed x : @closed T `]-oo, x].
Proof. by rewrite -setCitvr closedC. Qed.
Hint Resolve lray_closed : core.

Lemma itv_closed x y : closed `[x, y].
Lemma itv_closed x y : @closed T `[x, y].
Proof. by rewrite set_itv_splitI; apply: closedI => /=. Qed.
Hint Resolve itv_closed : core.

Expand Down