complement of finite in infinite is infinite

Stream: Is there code for X?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Very nice!

[Yakov Pechersky]

Should it be called infinite_compl_of_finite?

[Kevin Buzzard]

I just noticed this!

[Yakov Pechersky]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

:gemini:

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

oh no we don't

[Kevin Buzzard]

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

[Yakov Pechersky]

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]

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

[Kevin Buzzard]

A lem emoji would not be not useless.

[Yakov Pechersky]

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

[Kevin Buzzard]

so it seems!

[Kevin Buzzard]

or for :em:

[Adam Topaz]

[Kevin Buzzard]

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

[Kevin Buzzard]

#6266