search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
205 stars 45 forks source link

Missing notations in `itv.v`? #903

Open affeldt-aist opened 1 year ago

affeldt-aist commented 1 year ago

https://github.com/math-comp/analysis/blob/5d4db09b412ac521d67830bd1ba507aed567056c/theories/itv.v#L35-L40

I can find [itv of ...] but not [lb of ...], etc.

affeldt-aist commented 1 year ago

By the way, I was looking for a way to infer a {nonneg R} from a {i01 R}.

proux01 commented 1 year ago

I can find [itv of ...] but not [lb of ...], etc.

Indeed, they are apparently missing.

By the way, I was looking for a way to infer a {nonneg R} from a {i01 R}.

I guess the simplest solution would be to add a Canonical to be able to write x%:inum%:nng but the uncomfortable thing is: why would that instance take the lower bound rather than the upper bound? (other than the fact it is probably what one wants most fo the time)