equal
deleted
inserted
replaced
378 by auto |
378 by auto |
379 qed } |
379 qed } |
380 note * = this |
380 note * = this |
381 |
381 |
382 have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
382 have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
383 unfolding Liminf_def SUP_def |
383 unfolding Liminf_def |
384 by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
384 by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
385 (auto intro: eventually_True) |
385 (auto intro: eventually_True) |
386 also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
386 also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
387 by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
387 by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
388 (auto dest!: eventually_happens simp: F) |
388 (auto dest!: eventually_happens simp: F) |
403 by auto |
403 by auto |
404 qed } |
404 qed } |
405 note * = this |
405 note * = this |
406 |
406 |
407 have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
407 have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
408 unfolding Limsup_def INF_def |
408 unfolding Limsup_def |
409 by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
409 by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
410 (auto intro: eventually_True) |
410 (auto intro: eventually_True) |
411 also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
411 also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
412 by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
412 by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
413 (auto dest!: eventually_happens simp: F) |
413 (auto dest!: eventually_happens simp: F) |
427 by auto |
427 by auto |
428 with \<open>eventually P F\<close> F show False |
428 with \<open>eventually P F\<close> F show False |
429 by auto |
429 by auto |
430 qed |
430 qed |
431 have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
431 have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
432 unfolding Limsup_def INF_def |
432 unfolding Limsup_def |
433 by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
433 by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
434 (auto intro: eventually_True) |
434 (auto intro: eventually_True) |
435 also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
435 also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
436 by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
436 by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
437 (auto dest!: eventually_happens simp: F) |
437 (auto dest!: eventually_happens simp: F) |
453 by auto |
453 by auto |
454 qed } |
454 qed } |
455 note * = this |
455 note * = this |
456 |
456 |
457 have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
457 have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
458 unfolding Liminf_def SUP_def |
458 unfolding Liminf_def |
459 by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
459 by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
460 (auto intro: eventually_True) |
460 (auto intro: eventually_True) |
461 also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
461 also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
462 by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
462 by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
463 (auto dest!: eventually_happens simp: F) |
463 (auto dest!: eventually_happens simp: F) |