equal
deleted
inserted
replaced
1445 |
1445 |
1446 |
1446 |
1447 lemma landau_symbol_if_at_top_eq [simp]: |
1447 lemma landau_symbol_if_at_top_eq [simp]: |
1448 assumes "landau_symbol L L' Lr" |
1448 assumes "landau_symbol L L' Lr" |
1449 shows "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)" |
1449 shows "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)" |
1450 apply (rule landau_symbol.cong[OF assms]) |
1450 apply (rule landau_symbol.cong[OF assms]) |
1451 using less_add_one[of a] apply (auto intro: eventually_mono eventually_ge_at_top[of "a + 1"]) |
1451 by (auto simp add: frequently_def eventually_at_top_linorder dest!: spec [where x= "a + 1"]) |
1452 done |
|
1453 |
1452 |
1454 lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq] |
1453 lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq] |
1455 |
1454 |
1456 |
1455 |
1457 |
1456 |