## Stream: general

### Topic: Induction starting not at the bottom

#### 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 :=


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.

#### 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?

#### 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?

#### Mario Carneiro (Jan 14 2021 at 08:31):

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

#### Mario Carneiro (Jan 14 2021 at 08:32):

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

#### 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