## Stream: maths

### Topic: strange theorem

#### Kenny Lau (Apr 28 2018 at 05:27):

α : Type u,
A B : set α,
t : set (set α),

ht1 : t ⊆ {A},
ht2 : set.finite t,
ht3 : ⋂₀ t ⊆ B
⊢ A ⊆ B


#### Kenny Lau (Apr 28 2018 at 05:27):

claim: you can't prove it without using ht2

#### Kenny Lau (Apr 28 2018 at 05:29):

I mean, constructively, of course

#### Reid Barton (Apr 28 2018 at 05:29):

I was going to say, I'm pretty sure I can prove it, since I can use LEM :simple_smile:

#### Kenny Lau (Apr 28 2018 at 05:29):

:D

Last updated: May 11 2021 at 16:22 UTC