Limit_Superior_includes_Limit_Inferior
Provedlimits-inferiorlimits-superiorproofwikiset-theory
For a sequence of sets {E_n}, liminf E_n ⊆ limsup E_n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Limit_Superior_includes_Limit_Inferior {α : Type _} (E : ℕ → Set α) : (⋃ n, ⋂ m ≥ n, E m) ⊆ (⋂ n, ⋃ m ≥ n, E m) := by sorrySource