limit of a series of sets

Stream: general

[Simon Hudon]

I have an infinite series of sets that each include their successor and such that each is non-empty. How do I prove that the intersection of all sets is also non-empty?

variables
   (s : stream (set α))
   (h₀ : ∀ i, s i ≠ ∅)
   (h₁ : ∀ i, s (i+1) ⊆ s i)
example : (⋂ i, s i) ≠ ∅ := ...

[Mario Carneiro]

it's false? For example take s n := {m : nat // n <= m}

[Kenny Lau]

right, it’s false

[Kenny Lau]

i was thinking for 5 minutes whether it is true or false

[Kenny Lau]

take (0,1/n)

[Simon Hudon]

Damn it! You guys are right! I was hoping to generalize a theorem. I guess I'll have to keep thinking about restrictions

[Chris Hughes]

(deleted)