Common.Set.Intervals

Additional theorems around intervals.

theorem Set.Iio_nat_lt_ssubset {m : ℕ} {n : ℕ} (h : m < n) : Set.Iio m ⊂ Set.Iio n

If m < n then {0, …, m - 1} ⊂ {0, …, n - 1}.

theorem Set.SurjOn_emptyset_Iio_iff_eq_zero {α : Type u_1} {n : ℕ} {f : α → ℕ} : Set.SurjOn f ∅ (Set.Iio n) ↔ n = 0

It is never the case that the emptyset is surjective