Documentation

Mathlib.Tactic.Inclusion.Extension.IntervalInt.Basic

Basic inclusion extensions for interval_int #

This file defines basic operations for the interval_int inclusion family.

source
def Inclusion.IntervalInt.mkIntIVar :
InclusionExt

Construct an inclusion variable for an integer expression using an integer interval.

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