|
Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a. |
"Most of the important lemmas like this one are probably true of limf_sup. At least lime_sup_ge0,, lime_supD, lime_inf_sup, and lim_lime_inf. There may be some conditions to replace with \forall x \near F, but otherwise I'm hoping it just works." @zstone1
analysis/theories/realfun.v
Line 611 in 8196991
"Most of the important lemmas like this one are probably true of limf_sup. At least lime_sup_ge0,, lime_supD, lime_inf_sup, and lim_lime_inf. There may be some conditions to replace with
\forall x \near F, but otherwise I'm hoping it just works." @zstone1