Hi, thanks, I should really again the Euclid's Theorem tutorial. I fixed `i` and directly do induction on `j`, then it also worked with some cases analysis.
—Chun > Il giorno 05 gen 2019, alle ore 22:20, Konrad Slind <konrad.sl...@gmail.com> > ha scritto: > > There is discussion of something like this in the Euclid's Theorem tutorial. > You can do Induct_on `j - i` or do the trick where you prove ?k. j = i + SUC > k, eliminate j, and then induct on k. > > Konrad. > > > On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe) <binghe.l...@gmail.com > <mailto:binghe.l...@gmail.com>> wrote: > sorry, "i ≤ j” should be “i < j” actually: > > ∀i j. i < j ⇒ f (SUC i) ⊆ f j > ------------------------------------ > 0. ∀n. f n ⊆ f (SUC n) > 1. ∀n. 0 < n ⇒ f 0 ⊆ f n > > > Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) > > <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> ha scritto: > > > > Hi, > > > > I have the following goal to prove: (f : num -> ‘a set) > > > > ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j > > ------------------------------------ > > 0. ∀n. f n ⊆ f (SUC n) > > > > but how can I do the induction on … e.g. `j - i`? > > > > —Chun > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info > <https://lists.sourceforge.net/lists/listinfo/hol-info>
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
