# Zulip Chat Archive

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

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.

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