## Stream: new members

### Topic: cases on finite vs. infinite

#### Patrick Lutz (Jul 29 2020 at 18:44):

Suppose I know that some property holds when X is fintype and when X is infinite. How do I prove that it holds for all X? I am fine with using classical logic/choice if need be. MWE

constant foo : Type → Prop
axiom finite_foo (X : Type) [fintype X] : foo X
axiom infinite_foo (X : Type) [infinite X] : foo X

example (X : Type) : foo X := sorry


#### Kevin Buzzard (Jul 29 2020 at 18:45):

What's the definition of infinite? I don't have access to lean right now

#### Patrick Lutz (Jul 29 2020 at 18:46):

class infinite (α : Type*) : Prop :=
(not_fintype : fintype α → false)


#### Patrick Lutz (Jul 29 2020 at 18:47):

There's also set.infinite for saying a subset of a type X is infinite

#### Patrick Lutz (Jul 29 2020 at 18:47):

If I should be using that instead, that's fine too

#### Kevin Buzzard (Jul 29 2020 at 18:47):

The infinite class you quoted above just says not a fintype so it should be easy to do with that class

#### Kevin Buzzard (Jul 29 2020 at 18:48):

You can just do cases on nonempty (fintype X) right?

(deleted)

#### Patrick Lutz (Jul 29 2020 at 18:50):

Kevin Buzzard said:

You can just do cases on nonempty (fintype X) right?

Yeah, I guess that sounds right. I was trying to do cases on infinite and for some reason was getting stuck proving that something that's not infinite is fintype

#### Kevin Buzzard (Jul 29 2020 at 18:51):

You might want to look at where nonempty is defined because there will be a useful lemma in the API saying that if you're not nonempty then there's a map to false

#### Patrick Lutz (Jul 29 2020 at 18:55):

Kevin Buzzard said:

You might want to look at where nonempty is defined because there will be a useful lemma in the API saying that if you're not nonempty then there's a map to false

hmm, it looks like nonempty is in core/init/logic.lean but I don't see anything about having a map to false.

#### Kevin Buzzard (Jul 29 2020 at 18:57):

I want something which says not nonempty X -> (X -> false)

#### Patrick Lutz (Jul 29 2020 at 18:57):

okay, wait, I found it with library_search

#### Kevin Buzzard (Jul 29 2020 at 18:57):

Assume h : not nonempty X, intro x, apply h, use x

#### Kevin Buzzard (Jul 29 2020 at 18:58):

So that should be all you need

#### Patrick Lutz (Jul 29 2020 at 18:59):

not_nonempty_iff_imp_false

#### Patrick Lutz (Jul 29 2020 at 19:01):

Okay, now I have the proof

example (X : Type) : foo X :=
begin
by_cases h : nonempty (fintype X),
exact nonempty.elim h (λ (x : fintype X), @finite_foo X x),
exact @infinite_foo X (not_nonempty_fintype.mp h),
end


which seems simple enough to satisfy me. Thanks for the help @Kevin Buzzard!

#### Patrick Lutz (Jul 29 2020 at 19:01):

I think the main thing I didn't think of was doing cases on nonempty (fintype X) though in retrospect it makes sense I guess

Last updated: Dec 20 2023 at 11:08 UTC