notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
-interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x).
-interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
+interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).
(* 3.29 *)
definition lim ≝
notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
-interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x).
+interpretation "Excess lim" 'lim e s x = (lim e s x).
lemma sup_decreasing:
∀E:excess.∀xn:sequence E.