analysis icon indicating copy to clipboard operation
analysis copied to clipboard
verified publisher icon math-comp

`inf_lower_bound` and `inf_lb`

Open affeldt-aist opened this issue 1 year ago • 0 comments

non-homogeneous naming:

inf_lower_bound: forall [R : realType] [E : set R], has_inf E -> lbound E (inf E)
inf_lb: forall [R : realType] [E : set R], has_lbound E -> lbound E (inf E)

morover, is inf_lower_bound really interesting to have?

affeldt-aist avatar May 26 '24 08:05 affeldt-aist