Merge pull request #859 from affeldt-aist/ereal_20220227

\bar R canonicals for tblattice
math-comp · Feb 28, 2023 · 0e392b5 · 0e392b5
2 parents b82b9c3 + 6324d33
commit 0e392b5
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,10 @@
 
 ### Added
 
+- in `contructive_ereal.v`:
+  + lemmas `ereal_blatticeMixin`, `ereal_tblatticeMixin`
+  + canonicals `ereal_blatticeType`, `ereal_tblatticeType`
+
 ### Changed
 
 ### Renamed

diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
@@ -360,6 +360,16 @@ Canonical ereal_latticeType := LatticeType (extended R) le_total_ereal.
 Canonical ereal_distrLatticeType :=  DistrLatticeType (extended R) le_total_ereal.
 Canonical ereal_orderType := OrderType (extended R) le_total_ereal.
 
+Lemma ereal_blatticeMixin :
+  Order.BLattice.mixin_of (Order.POrder.class (@ereal_porderType R)).
+Proof. by exists -oo; exact leNye. Qed.
+Canonical ereal_blatticeType := BLatticeType (extended R) ereal_blatticeMixin.
+
+Lemma ereal_tblatticeMixin :
+  Order.TBLattice.mixin_of (Order.POrder.class ereal_blatticeType).
+Proof. by exists +oo; exact leey. Qed.
+Canonical ereal_tblatticeType := TBLatticeType (extended R) ereal_tblatticeMixin.
+
 End ERealOrder_realDomainType.
 
 Section ERealArith.