# Zulip Chat Archive

## Stream: general

### Topic: Induction on a set

#### Alice Laroche (Nov 29 2021 at 12:06):

Hello,

I have absolutly no idea on how i can prove this, can i have some help ?

```
theorem prop_on_inductive_set
(T : Type)
(B X : set T)
(f : T -> T)
(P : T -> Prop)
(h₁ : X = B ∪ f '' X)
(h₂ : ∀x ∈ B, P x)
(h₃ : ∀x, P x -> P (f x))
: ∀x ∈ X, P x :=
begin
sorry,
end
```

#### Anne Baanen (Nov 29 2021 at 12:09):

Do you have a proof on paper already?

#### Alice Laroche (Nov 29 2021 at 12:21):

No, it was assumed in the lecture

#### Anne Baanen (Nov 29 2021 at 12:22):

Ah, I see. Because the hypotheses are probably not saying what you want to say: if `B = ∅`

and `f = id`

then the hypotheses hold for all `T`

, `B`

, `P`

, `x`

, in particular `P = λ x, false`

.

#### Anne Baanen (Nov 29 2021 at 12:24):

In particular, `h₁`

should be something like "`X`

contains the elements of `B`

with `f`

applied a *finite* number of times to them". (And then you'd be able to apply induction to the number of times you apply `f`

.)

#### Anne Baanen (Nov 29 2021 at 12:25):

The counterexample:

```
import data.set
theorem prop_on_inductive_set
(h : Π (T : Type) (B X : set T) (f : T -> T) (P : T -> Prop) (h₁ : X = B ∪ f '' X) (h₂ : ∀x ∈ B, P x) (h₃ : ∀x, P x -> P (f x)), ∀x ∈ X, P x) :
false :=
begin
refine h ℕ ∅ ⊤ id (λ _, false) _ _ _ 0 (set.mem_univ 0),
{ simp },
{ rintro x ⟨⟩ },
{ intros x h, exact h }
end
```

#### Anne Baanen (Nov 29 2021 at 12:27):

So this is probably what you want to prove instead:

```
import data.set
theorem prop_on_inductive_set
(T : Type) (B X : set T) (f : T -> T) (P : T -> Prop)
(h₁ : ∀ x ∈ X, ∃ (b ∈ B) (n : ℕ), (f^[n]) b = x)
(h₂ : ∀x ∈ B, P x)
(h₃ : ∀x, P x -> P (f x)) :
∀x ∈ X, P x :=
begin
sorry
end
```

#### Alice Laroche (Nov 29 2021 at 12:32):

Oooh, yes , this is what i want to prove indeed, I wanted to prove the thing as it was write in our lecture, without thinking of the formal definition of the notation. Thank you.

#### Patrick Johnson (Nov 29 2021 at 13:39):

Proof:

#### Alice Laroche (Nov 29 2021 at 14:04):

Whoaa, this is way better than mine, thank you too.

#### Eric Wieser (Nov 29 2021 at 23:27):

~~Isn't that ~~ nevermind`iter_succ`

just the equation lemma for docs#nat.iterate?

#### Eric Wieser (Nov 29 2021 at 23:31):

It's actually docs#function.commute.iterate_left, as `(function.commute.refl f).iterate_left n`

Last updated: Dec 20 2023 at 11:08 UTC