strange theorem

Stream: maths

[Kenny Lau]

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

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

[Kenny Lau]

claim: you can't prove it without using ht2

[Kenny Lau]

I mean, constructively, of course

[Reid Barton]

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

[Kenny Lau]

:D