## Stream: Is there code for X?

### Topic: complement of finite in infinite is infinite

#### Kevin Buzzard (Feb 16 2021 at 16:36):

I am not using finset in my teaching, I'm using set.finite because Props are less scary. Do we have this:

lemma infinite_of_finite_compl {α : Type} [infinite α] {s : set α}
(hs : s.finite) : sᶜ.infinite :=
begin
sorry
end


? I can't find it but I'm still not sure I know all the places where this stuff is talked about.

#### Yakov Pechersky (Feb 16 2021 at 16:44):

lemma infinite_of_finite_compl {α : Type} [infinite α] {s : set α}
(hs : s.finite) : sᶜ.infinite :=
λ h, set.infinite_univ (by simpa using hs.union h)


Very nice!

#### Yakov Pechersky (Feb 16 2021 at 17:22):

Should it be called infinite_compl_of_finite?

#### Kevin Buzzard (Feb 16 2021 at 17:22):

I just noticed this!

#### Yakov Pechersky (Feb 16 2021 at 17:22):

Unless I guess you're taking advantage that compl \o compl = id

#### Kevin Buzzard (Feb 16 2021 at 17:22):

when would I ever use the law of the excluded middle!

:gemini:

#### Kevin Buzzard (Feb 16 2021 at 17:23):

lemma infinite_of_finite_compl {α : Type} [infinite α] {s : set α}
(hs : sᶜ.finite) : s.infinite :=
λ h, set.infinite_univ (by simpa using hs.union h)

lemma compl_infinite_of_finite {α : Type} [infinite α] {s : set α}
(hs : s.finite) : sᶜ.infinite :=
λ h, set.infinite_univ (by simpa using hs.union h)


#### Yakov Pechersky (Feb 16 2021 at 17:23):

(we need an :lem: or :em: emoji)

oh no we don't

#### Kevin Buzzard (Feb 16 2021 at 17:24):

we need a not :lem: emoji, oh maybe we have one: :warning:

#### Yakov Pechersky (Feb 16 2021 at 17:24):

infinite_compl for the latter? It's always not clear to me how the naming should work on predicates that are always accessed via dot-projection notation

#### Kevin Buzzard (Feb 16 2021 at 17:25):

Right now we have compl_univ and compl_inter but I see what you mean.

#### Kevin Buzzard (Feb 16 2021 at 17:26):

A lem emoji would not be not useless.

#### Yakov Pechersky (Feb 16 2021 at 17:27):

so :lemon: for :lem:, :gemini: for :em:, :deciduous_tree: for :decidable:

so it seems!

or for :em:

#### Kevin Buzzard (Feb 16 2021 at 17:34):

that should be called not not not, not not not.

#### Kevin Buzzard (Feb 16 2021 at 17:39):

#6266

Last updated: May 17 2021 at 15:13 UTC