Hypothesis operations for integer intervals

This file defines the hypothesis extensions for interval_int.

theorem Inclusion.IntervalInt.Iic_mem_of_le {x y : ℤ} {I : Interval ℤ} (hxy : x ≤ y) (hy : y ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalInt.Ici_mem_of_le {x y : ℤ} {I : Interval ℤ} (hxy : x ≤ y) (hx : x ∈ I) : y ∈ Interval.Ici I.lb

theorem Inclusion.IntervalInt.Iic_mem_of_lt {x y : ℤ} {I : Interval ℤ} (hxy : x < y) (hy : y ∈ I) : x ∈ Interval.Iic (I.ub - 1)

theorem Inclusion.IntervalInt.Ici_mem_of_lt {x y : ℤ} {I : Interval ℤ} (hxy : x < y) (hx : x ∈ I) : y ∈ Interval.Ici (I.lb + 1)

theorem Inclusion.IntervalInt.Ici_mem_of_mem_Ici {a x : ℤ} {I : Interval ℤ} (hx : x ∈ Set.Ici a) (ha : a ∈ I) : x ∈ Interval.Ici I.lb

theorem Inclusion.IntervalInt.Ici_mem_of_mem_Ioi {a x : ℤ} {I : Interval ℤ} (hx : x ∈ Set.Ioi a) (ha : a ∈ I) : x ∈ Interval.Ici (I.lb + 1)

theorem Inclusion.IntervalInt.Iic_mem_of_mem_Iic {b x : ℤ} {I : Interval ℤ} (hx : x ∈ Set.Iic b) (hb : b ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalInt.Iic_mem_of_mem_Iio {b x : ℤ} {I : Interval ℤ} (hx : x ∈ Set.Iio b) (hb : b ∈ I) : x ∈ Interval.Iic (I.ub - 1)

theorem Inclusion.IntervalInt.Icc_mem_of_mem_Icc {a b x : ℤ} {I J : Interval ℤ} (hx : x ∈ Set.Icc a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc I.lb J.ub

theorem Inclusion.IntervalInt.Icc_mem_of_mem_Ico {a b x : ℤ} {I J : Interval ℤ} (hx : x ∈ Set.Ico a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc I.lb (J.ub - 1)

theorem Inclusion.IntervalInt.Icc_mem_of_mem_Ioc {a b x : ℤ} {I J : Interval ℤ} (hx : x ∈ Set.Ioc a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc (I.lb + 1) J.ub

theorem Inclusion.IntervalInt.Icc_mem_of_mem_Ioo {a b x : ℤ} {I J : Interval ℤ} (hx : x ∈ Set.Ioo a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc (I.lb + 1) (J.ub - 1)