Zulip Chat Archive

Stream: new members

Topic: Easier way to show superset of infinite set is infinite?


view this post on Zulip Patrick Lutz (Aug 05 2020 at 18:01):

I want to show that if sts \subseteq t and ss is infinite then so is tt. I can do so as follows

import data.set.finite

example (X : Type) (s : set X) (t : set X) (hst : s  t) (hs : s.infinite) : t.infinite :=
begin
    revert hs,
    contrapose,
    intro ht,
    have : s.finite := set.finite.subset (show t.finite, by finish) hst,
    tauto,
end

But it's a little annoying, especially if I want to use it in the middle of some other proof. Is there a better way to do this? I don't mind using classical logic btw.

view this post on Zulip Patrick Lutz (Aug 05 2020 at 18:01):

Also, in the above example, how can I get contrapose! to give me t.finite → s.finite instead of ¬t.infinite → ¬s.infinite? Once again, I don't mind using classical logic.

view this post on Zulip Reid Barton (Aug 05 2020 at 18:19):

Rather than contrapose, you can just apply mt

view this post on Zulip Reid Barton (Aug 05 2020 at 18:21):

example (X : Type) (s : set X) (t : set X) (hst : s  t) (hs : s.infinite) : t.infinite :=
mt (λ ht, ht.subset hst) hs

Last updated: May 14 2021 at 22:15 UTC