## Stream: new members

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

#### Patrick Lutz (Aug 05 2020 at 18:01):

I want to show that if $s \subseteq t$ and $s$ is infinite then so is $t$. 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.

#### 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.

#### Reid Barton (Aug 05 2020 at 18:19):

Rather than contrapose, you can just apply mt

#### 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