waynee95 (Oct 19 2022 at 18:32): waynee95 (Oct 19 2022 at 18:32):Is there a shorter way to arrive at the induction here?
lemma blubb:
assumes "∀i ≤ card S + 1. ∀i' ≤ card S + 1.
i ≠ i' ⟶ (f::nat⇒'a) i ≠ f i'"
shows "∀n ≤ card S + 1. n ≤ card (⋃i≤n. {f i})"
proof (rule allI, rule impI)
fix n
show "n ≤ card S + 1 ⟹ n ≤ card (⋃i≤n. {f i})"
proof (induction n)
...
Something like proof (rule allI, rule impI, induction) or proof (rule allI, rule impI, induction n) does not work and I can see why.
Maybe it's not really important to save two lines here but I just wanted to check.
Mathias Fleury (Oct 19 2022 at 18:38):Theoretically, induct_tac might work
Mathias Fleury (Oct 19 2022 at 18:38):otherwise, rephrase your theorem by removing the ∀
waynee95 (Oct 19 2022 at 18:41):induct_tac did something but not something right.
But rephrasing the theorem by removing the quantifier works...
lemma blubb:
assumes "∀i ≤ card S + 1. ∀i' ≤ card S + 1.
i ≠ i' ⟶ (f::nat⇒'a) i ≠ f i'"
shows "n ≤ card S + 1 ⟹ n ≤ card (⋃i≤n. {f i})"
proof (induction n)
well that was easier than I expected whoops
Last updated: Apr 20 2024 at 04:19 UTC