Hypothesis operations for dyadic real intervals

This file defines the hypothesis extensions for the interval_dyadic_real inclusion family.

theorem Inclusion.IntervalDyadicReal.Iic_mem_of_le {x y : ℝ} {I : Interval Dyadic} (hxy : x ≤ y) (hy : y ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalDyadicReal.Ici_mem_of_le {x y : ℝ} {I : Interval Dyadic} (hxy : x ≤ y) (hx : x ∈ I) : y ∈ Interval.Ici I.lb

theorem Inclusion.IntervalDyadicReal.Iic_mem_of_lt {x y : ℝ} {I : Interval Dyadic} (hxy : x < y) (hy : y ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalDyadicReal.Ici_mem_of_lt {x y : ℝ} {I : Interval Dyadic} (hxy : x < y) (hx : x ∈ I) : y ∈ Interval.Ici I.lb

theorem Inclusion.IntervalDyadicReal.Ici_mem_of_mem_Ici {a x : ℝ} {I : Interval Dyadic} (hx : x ∈ Set.Ici a) (ha : a ∈ I) : x ∈ Interval.Ici I.lb

theorem Inclusion.IntervalDyadicReal.Ici_mem_of_mem_Ioi {a x : ℝ} {I : Interval Dyadic} (hx : x ∈ Set.Ioi a) (ha : a ∈ I) : x ∈ Interval.Ici I.lb

theorem Inclusion.IntervalDyadicReal.Iic_mem_of_mem_Iic {b x : ℝ} {I : Interval Dyadic} (hx : x ∈ Set.Iic b) (hb : b ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalDyadicReal.Iic_mem_of_mem_Iio {b x : ℝ} {I : Interval Dyadic} (hx : x ∈ Set.Iio b) (hb : b ∈ I) : x ∈ Interval.Iic I.ub

theorem Inclusion.IntervalDyadicReal.Icc_mem_of_mem_Ico {a b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ Set.Ico a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc I.lb J.ub

theorem Inclusion.IntervalDyadicReal.Icc_mem_of_mem_Ioc {a b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ Set.Ioc a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc I.lb J.ub

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

theorem Inclusion.IntervalDyadicReal.Icc_mem_of_mem_Ioo {a b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ Set.Ioo a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Interval.Icc I.lb J.ub