Zulip Chat Archive

Stream: maths

Topic: strange theorem


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

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:27):

claim: you can't prove it without using ht2

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:29):

I mean, constructively, of course

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

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:29):

:D


Last updated: May 11 2021 at 16:22 UTC