From 907c539c04bf0ca0d493f77cd7b57159f81b69da Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 5 Feb 2026 16:21:18 +0900 Subject: [PATCH 1/3] fix itv_closed_ends --- classical/set_interval.v | 2 +- theories/topology_theory/order_topology.v | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/classical/set_interval.v b/classical/set_interval.v index 3f21bbf46..7008aadd0 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -850,7 +850,7 @@ Implicit Types (i : interval T). Definition itv_is_closed_unbounded i : bool := match i with - | `[_, +oo[ | `]-oo, _[ | `]-oo, +oo[ => true + | `[_, +oo[ | `]-oo, _] | `]-oo, +oo[ => true | _ => false end. diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 0658f12ce..eafb9197a 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -111,6 +111,10 @@ Lemma itv_closed x y : @closed T `[x, y]. Proof. by rewrite set_itv_splitI; apply: closedI => /=. Qed. Hint Resolve itv_closed : core. +Lemma itv_closed_ends_closed (i : interval T) : + itv_closed_ends i -> closed [set` i]. +Proof. by case: i => [[[]t1|[]]] [[]t2|[]]. Qed. + Lemma itv_closure x y : closure `]x, y[ `<=` `[x, y]. Proof. rewrite closureE => r; apply; split => //. From b1c1a56a45a6314ee5d3c6ee684a66775aa1500d Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 5 Feb 2026 16:44:06 +0900 Subject: [PATCH 2/3] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0d911f46c..a005fa095 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,6 +3,9 @@ ## [Unreleased] ### Added +- in order_topology.v + + lemma `itv_closed_ends_closed` + - in set_interval.v + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends` From 579d32eccb24cf62989382bea815f3995f77fe3d Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 5 Feb 2026 16:45:40 +0900 Subject: [PATCH 3/3] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a005fa095..b7fcc4b73 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,9 @@ + lemma `RlnE` ### Changed +- in set_interval.v + + `itv_is_closed_unbounded` (fix the definition) + - in set_interval.v + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)