Documentation

Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Basic

Basic inclusion extensions for interval_dyadic_real #

This file defines basic operations for the interval_dyadic_real inclusion family.

source
def Inclusion.IntervalDyadicReal.mkRealIVar :
InclusionExt

Construct an inclusion variable for a real expression using a dyadic interval.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Inclusion.IntervalDyadicReal.mem_iff_mem_map {x : ℝ} {I : Interval Dyadic} :
    x ∈ I ↔ x ∈ I.map Dyadic.toReal
    source
    theorem Inclusion.IntervalDyadicReal.natCast_mem (n : ℕ) :
    ↑n ∈ Interval.singleton ↑n
    source
    theorem Inclusion.IntervalDyadicReal.ofNat_mem (n : ℕ) :
    OfNat.ofNat n ∈ Interval.singleton ↑n
    source
    theorem Inclusion.IntervalDyadicReal.intCast_mem (z : ℤ) :
    ↑z ∈ Interval.singleton ↑z
    source
    theorem Inclusion.IntervalDyadicReal.add_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x + y ∈ I.add J
    source
    theorem Inclusion.IntervalDyadicReal.neg_mem {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) :
    -x ∈ I.neg
    source
    theorem Inclusion.IntervalDyadicReal.abs_mem {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) :
    |x| ∈ I.abs
    source
    theorem Inclusion.IntervalDyadicReal.sub_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x - y ∈ I.sub J
    source
    theorem Inclusion.IntervalDyadicReal.mul_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x * y ∈ I.mul J
    source
    theorem Inclusion.IntervalDyadicReal.le_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x ≤ y ∈ I.le J
    source
    theorem Inclusion.IntervalDyadicReal.lt_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x < y ∈ I.lt J
    source
    theorem Inclusion.IntervalDyadicReal.eq_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) :
    x = y ∈ I.eq J
    source
    theorem Inclusion.IntervalDyadicReal.mem_Ici {a x : ℝ} {I J : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) :
    (x ∈ Set.Ici a) ∈ I.le J
    source
    theorem Inclusion.IntervalDyadicReal.mem_Ioi {a x : ℝ} {I J : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) :
    (x ∈ Set.Ioi a) ∈ I.lt J
    source
    theorem Inclusion.IntervalDyadicReal.mem_Iic {b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hb : b ∈ J) :
    (x ∈ Set.Iic b) ∈ I.le J
    source
    theorem Inclusion.IntervalDyadicReal.mem_Iio {b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hb : b ∈ J) :
    (x ∈ Set.Iio b) ∈ I.lt J
    source
    theorem Inclusion.IntervalDyadicReal.mem_Icc {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) :
    (x ∈ Set.Icc a b) ∈ (I.le J).and (J.le K)
    source
    theorem Inclusion.IntervalDyadicReal.mem_Ico {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) :
    (x ∈ Set.Ico a b) ∈ (I.le J).and (J.lt K)
    source
    theorem Inclusion.IntervalDyadicReal.mem_Ioc {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) :
    (x ∈ Set.Ioc a b) ∈ (I.lt J).and (J.le K)
    source
    theorem Inclusion.IntervalDyadicReal.mem_Ioo {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) :
    (x ∈ Set.Ioo a b) ∈ (I.lt J).and (J.lt K)