fix itv_closed_ends

CHANGELOG_UNRELEASED.md

@@ -3,13 +3,19 @@
 ## [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`
 
 - in `Rstruct_topology.v`:
   + 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)
 

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.
 

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 => //.