Zulip Chat Archive

Stream: general

Topic: Induction starting not at the bottom


view this post on Zulip Chase Meadors (Jan 14 2021 at 08:13):

Is there an easy way to perform induction with a "different starting element"? (easy = without writing a lemma :wink: ). Perhaps some way to leverage the existing induction theorem?
In my case, I want to prove something about nonempty finsets. Namely, that finite sup in a directed set stays in the directed set:

lemma test {α : Type} [decidable_eq α] [complete_lattice α] (S : set α) (hdir : directed_on () S)
  (F : finset α) (hemp : F.nonempty) (hF : F  S) : F.sup id  S :=

I'd love to start with

apply finset.induction F,

but alas, this is only necessarily true for nonempty finsets.
I've had the same case before when wanting to prove something about positive naturals, so I thought I'd ask for some tips.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 08:22):

You can probably just use the usual induction principle in any given case. Or you can just write your own and apply it. Why do you think the usual induction principle won't work for you? I think that all other induction principles are derived from it, in some sense. What happens after applying finset.induction? The base case should be provable by contradiction, no?

view this post on Zulip Chase Meadors (Jan 14 2021 at 08:30):

Well, the base case here needs ⊥ ∈ S, which I have no reason to assume for an arbitrary directed set S. But, I think I see what you're saying - namely a "custom" induction principle will not be hard to write since it can simply use the regular one?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:31):

You just prove by induction that ⊥ ∈ S -> P S

view this post on Zulip Mario Carneiro (Jan 14 2021 at 08:32):

the implication ensures that the case S = ⊥ is vacuously true

view this post on Zulip Chase Meadors (Jan 14 2021 at 08:34):

Ah, that's perfect! I had tried something like that in proving the implication F.nonempty -> F.sup id in S by induction, but rather your proposition is what I need. Thanks!
Well, wait, this would still ensure I need bottom in S anywhere to apply it...


Last updated: May 08 2021 at 19:11 UTC