search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
191 stars 41 forks source link

notation for intervals #795

Open affeldt-aist opened 1 year ago

affeldt-aist commented 1 year ago

We have been using intervals with extended real numbers but this has the consequence that `[0%E, +oo] = `[0%E, +oo[. How can we handle that? @hoheinzollern @t6s

t6s commented 1 year ago

Is it difficult to modify the notation on the LHS to `[_, +oo[ to be consistent?

CohenCyril commented 1 year ago

I suggest you overload notations in ereal scope and print `[x, +oo[%O for ereals differently.

CohenCyril commented 1 year ago

Or one could implement a latticeWithNoTop in the same way as https://github.com/coq/coq/blob/master/theories/ssr/ssreflect.v#L30-L34