Zulip Chat Archive

Stream: Is there code for X?

Topic: complement of finite in infinite is infinite


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:19):

Very nice!

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:22):

Should it be called infinite_compl_of_finite?

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:22):

I just noticed this!

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:22):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:22):

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

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:23):

:gemini:

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:23):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:23):

oh no we don't

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:24):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:25):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:26):

A lem emoji would not be not useless.

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:27):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:27):

so it seems!

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:28):

or :emacs: for :em:

view this post on Zulip Adam Topaz (Feb 16 2021 at 17:33):

:not_not:

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:34):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:39):

#6266


Last updated: May 17 2021 at 15:13 UTC