src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 54260 6a967667fd45
parent 54258 adfc759263ab
child 55522 23d2cbac6dce
equal deleted inserted replaced
54259:71c701dc5bf9 54260:6a967667fd45
  1207   shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
  1207   shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
  1208   unfolding inf_min[symmetric] Liminf_at
  1208   unfolding inf_min[symmetric] Liminf_at
  1209   apply (subst inf_commute)
  1209   apply (subst inf_commute)
  1210   apply (subst SUP_inf)
  1210   apply (subst SUP_inf)
  1211   apply (intro SUP_cong[OF refl])
  1211   apply (intro SUP_cong[OF refl])
  1212   apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
  1212   apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
  1213   apply (simp add: INF_def del: inf_ereal_def)
  1213   apply (simp add: INF_def del: inf_ereal_def)
  1214   done
  1214   done
  1215 
  1215 
  1216 
  1216 
  1217 subsection {* monoset *}
  1217 subsection {* monoset *}