mathlib docs: core.init.data.int.order

source

def int.le :

ℤ → ℤ → Prop

Equations

a.le b = nonneg (b - a)

source

@[instance]

def int.has_le :

has_le ℤ

Equations

int.has_le = {le := int.le}

source

def int.lt :

ℤ → ℤ → Prop

Equations

a.lt b = (a + 1 ≤ b)

source

@[instance]

def int.has_lt :

has_lt ℤ

Equations

int.has_lt = {lt := int.lt}

source

@[instance]

def int.decidable_le (a b : ℤ) :

decidable (a ≤ b)

Equations

a.decidable_le b = decidable_nonneg (b - a)

source

@[instance]

def int.decidable_lt (a b : ℤ) :

decidable (a < b)

Equations

a.decidable_lt b = decidable_nonneg (b - (a + 1))

source

theorem int.lt_iff_add_one_le (a b : ℤ) :

a < b ↔ a + 1 ≤ b

source

theorem int.le.intro_sub {a b : ℤ} {n : ℕ} :

b - a = ↑n → a ≤ b

source

theorem int.le.intro {a b : ℤ} {n : ℕ} :

a + ↑n = b → a ≤ b

source

theorem int.le.dest_sub {a b : ℤ} :

a ≤ b → (∃ (n : ℕ), b - a = ↑n)

source

theorem int.le.dest {a b : ℤ} :

a ≤ b → (∃ (n : ℕ), a + ↑n = b)

source

theorem int.le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} :

(∀ (n : ℕ), a + ↑n = b → P) → P

source

theorem int.le_total (a b : ℤ) :

a ≤ b ∨ b ≤ a

source

theorem int.coe_nat_le_coe_nat_of_le {m n : ℕ} :

m ≤ n → ↑m ≤ ↑n

source

theorem int.le_of_coe_nat_le_coe_nat {m n : ℕ} :

↑m ≤ ↑n → m ≤ n

source

theorem int.coe_nat_le_coe_nat_iff (m n : ℕ) :

↑m ≤ ↑n ↔ m ≤ n

source

theorem int.coe_zero_le (n : ℕ) :

0 ≤ ↑n

source

theorem int.eq_coe_of_zero_le {a : ℤ} :

0 ≤ a → (∃ (n : ℕ), a = ↑n)

source

theorem int.eq_succ_of_zero_lt {a : ℤ} :

0 < a → (∃ (n : ℕ), a = ↑(n.succ))

source

theorem int.lt_add_succ (a : ℤ) (n : ℕ) :

a < a + ↑(n.succ)

source

theorem int.lt.intro {a b : ℤ} {n : ℕ} :

a + ↑(n.succ) = b → a < b

source

theorem int.lt.dest {a b : ℤ} :

a < b → (∃ (n : ℕ), a + ↑(n.succ) = b)

source

theorem int.lt.elim {a b : ℤ} (h : a < b) {P : Prop} :

(∀ (n : ℕ), a + ↑(n.succ) = b → P) → P

source

theorem int.coe_nat_lt_coe_nat_iff (n m : ℕ) :

↑n < ↑m ↔ n < m

source

theorem int.lt_of_coe_nat_lt_coe_nat {m n : ℕ} :

↑m < ↑n → m < n

source

theorem int.coe_nat_lt_coe_nat_of_lt {m n : ℕ} :

m < n → ↑m < ↑n

source

theorem int.le_refl (a : ℤ) :

a ≤ a

source

theorem int.le_trans {a b c : ℤ} :

a ≤ b → b ≤ c → a ≤ c

source

theorem int.le_antisymm {a b : ℤ} :

a ≤ b → b ≤ a → a = b

source

theorem int.lt_irrefl (a : ℤ) :

¬a < a

source

theorem int.ne_of_lt {a b : ℤ} :

a < b → a ≠ b

source

theorem int.le_of_lt {a b : ℤ} :

a < b → a ≤ b

source

theorem int.lt_iff_le_and_ne (a b : ℤ) :

a < b ↔ a ≤ b ∧ a ≠ b

source

theorem int.lt_succ (a : ℤ) :

a < a + 1

source

theorem int.add_le_add_left {a b : ℤ} (h : a ≤ b) (c : ℤ) :

c + a ≤ c + b

source

theorem int.add_lt_add_left {a b : ℤ} (h : a < b) (c : ℤ) :

c + a < c + b

source

theorem int.mul_nonneg {a b : ℤ} :

0 ≤ a → 0 ≤ b → 0 ≤ a * b

source

theorem int.mul_pos {a b : ℤ} :

0 < a → 0 < b → 0 < a * b

source

theorem int.zero_lt_one :

0 < 1

source

theorem int.lt_iff_le_not_le {a b : ℤ} :

a < b ↔ a ≤ b ∧ ¬b ≤ a

source

@[instance]

def int.decidable_linear_order :

decidable_linear_order ℤ

Equations

source

theorem int.eq_nat_abs_of_zero_le {a : ℤ} :

0 ≤ a → a = ↑(a.nat_abs)

source

theorem int.le_nat_abs {a : ℤ} :

a ≤ ↑(a.nat_abs)

source

theorem int.neg_succ_lt_zero (n : ℕ) :

-[1+ n] < 0

source

theorem int.eq_neg_succ_of_lt_zero {a : ℤ} :

a < 0 → (∃ (n : ℕ), a = -[1+ n])

source

theorem int.eq_neg_of_eq_neg {a b : ℤ} :

a = -b → b = -a

source

theorem int.neg_add_cancel_left (a b : ℤ) :

-a + (a + b) = b

source

theorem int.add_neg_cancel_left (a b : ℤ) :

a + (-a + b) = b

source

theorem int.add_neg_cancel_right (a b : ℤ) :

a + b + -b = a

source

theorem int.neg_add_cancel_right (a b : ℤ) :

a + -b + b = a

source

theorem int.sub_self (a : ℤ) :

a - a = 0

source

theorem int.sub_eq_zero_of_eq {a b : ℤ} :

a = b → a - b = 0

source

theorem int.eq_of_sub_eq_zero {a b : ℤ} :

a - b = 0 → a = b

source

theorem int.sub_eq_zero_iff_eq {a b : ℤ} :

a - b = 0 ↔ a = b

source

@[simp]

theorem int.neg_eq_of_add_eq_zero {a b : ℤ} :

a + b = 0 → -a = b

source

theorem int.neg_mul_eq_neg_mul (a b : ℤ) :

-(a * b) = -a * b

source

theorem int.neg_mul_eq_mul_neg (a b : ℤ) :

-(a * b) = a * -b

source

@[simp]

theorem int.neg_mul_eq_neg_mul_symm (a b : ℤ) :

-a * b = -(a * b)

source

@[simp]

theorem int.mul_neg_eq_neg_mul_symm (a b : ℤ) :

a * -b = -(a * b)

source

theorem int.neg_mul_neg (a b : ℤ) :

-a * -b = a * b

source

theorem int.neg_mul_comm (a b : ℤ) :

-a * b = a * -b

source

theorem int.mul_sub (a b c : ℤ) :

a * (b - c) = a * b - a * c

source

theorem int.sub_mul (a b c : ℤ) :

(a - b) * c = a * c - b * c

source

theorem int.le_of_add_le_add_left {a b c : ℤ} :

a + b ≤ a + c → b ≤ c

source

theorem int.lt_of_add_lt_add_left {a b c : ℤ} :

a + b < a + c → b < c

source

theorem int.add_le_add_right {a b : ℤ} (h : a ≤ b) (c : ℤ) :

a + c ≤ b + c

source

theorem int.add_lt_add_right {a b : ℤ} (h : a < b) (c : ℤ) :

a + c < b + c

source

theorem int.add_le_add {a b c d : ℤ} :

a ≤ b → c ≤ d → a + c ≤ b + d

source

theorem int.le_add_of_nonneg_right {a b : ℤ} :

b ≥ 0 → a ≤ a + b

source

theorem int.le_add_of_nonneg_left {a b : ℤ} :

b ≥ 0 → a ≤ b + a

source

theorem int.add_lt_add {a b c d : ℤ} :

a < b → c < d → a + c < b + d

source

theorem int.add_lt_add_of_le_of_lt {a b c d : ℤ} :

a ≤ b → c < d → a + c < b + d

source

theorem int.add_lt_add_of_lt_of_le {a b c d : ℤ} :

a < b → c ≤ d → a + c < b + d

source

theorem int.lt_add_of_pos_right (a : ℤ) {b : ℤ} :

b > 0 → a < a + b

source

theorem int.lt_add_of_pos_left (a : ℤ) {b : ℤ} :

b > 0 → a < b + a

source

theorem int.le_of_add_le_add_right {a b c : ℤ} :

a + b ≤ c + b → a ≤ c

source

theorem int.lt_of_add_lt_add_right {a b c : ℤ} :

a + b < c + b → a < c

source

theorem int.add_nonneg {a b : ℤ} :

0 ≤ a → 0 ≤ b → 0 ≤ a + b

source

theorem int.add_pos {a b : ℤ} :

0 < a → 0 < b → 0 < a + b

source

theorem int.add_pos_of_pos_of_nonneg {a b : ℤ} :

0 < a → 0 ≤ b → 0 < a + b

source

theorem int.add_pos_of_nonneg_of_pos {a b : ℤ} :

0 ≤ a → 0 < b → 0 < a + b

source

theorem int.add_nonpos {a b : ℤ} :

a ≤ 0 → b ≤ 0 → a + b ≤ 0

source

theorem int.add_neg {a b : ℤ} :

a < 0 → b < 0 → a + b < 0

source

theorem int.add_neg_of_neg_of_nonpos {a b : ℤ} :

a < 0 → b ≤ 0 → a + b < 0

source

theorem int.add_neg_of_nonpos_of_neg {a b : ℤ} :

a ≤ 0 → b < 0 → a + b < 0

source

theorem int.lt_add_of_le_of_pos {a b c : ℤ} :

b ≤ c → 0 < a → b < c + a

source

theorem int.sub_add_cancel (a b : ℤ) :

a - b + b = a

source

theorem int.add_sub_cancel (a b : ℤ) :

a + b - b = a

source

theorem int.add_sub_assoc (a b c : ℤ) :

a + b - c = a + (b - c)

source

theorem int.neg_le_neg {a b : ℤ} :

a ≤ b → -b ≤ -a

source

theorem int.le_of_neg_le_neg {a b : ℤ} :

-b ≤ -a → a ≤ b

source

theorem int.nonneg_of_neg_nonpos {a : ℤ} :

-a ≤ 0 → 0 ≤ a

source

theorem int.neg_nonpos_of_nonneg {a : ℤ} :

0 ≤ a → -a ≤ 0

source

theorem int.nonpos_of_neg_nonneg {a : ℤ} :

0 ≤ -a → a ≤ 0

source

theorem int.neg_nonneg_of_nonpos {a : ℤ} :

a ≤ 0 → 0 ≤ -a

source

theorem int.neg_lt_neg {a b : ℤ} :

a < b → -b < -a

source

theorem int.lt_of_neg_lt_neg {a b : ℤ} :

-b < -a → a < b

source

theorem int.pos_of_neg_neg {a : ℤ} :

-a < 0 → 0 < a

source

theorem int.neg_neg_of_pos {a : ℤ} :

0 < a → -a < 0

source

theorem int.neg_of_neg_pos {a : ℤ} :

0 < -a → a < 0

source

theorem int.neg_pos_of_neg {a : ℤ} :

a < 0 → 0 < -a

source

theorem int.le_neg_of_le_neg {a b : ℤ} :

a ≤ -b → b ≤ -a

source

theorem int.neg_le_of_neg_le {a b : ℤ} :

-a ≤ b → -b ≤ a

source

theorem int.lt_neg_of_lt_neg {a b : ℤ} :

a < -b → b < -a

source

theorem int.neg_lt_of_neg_lt {a b : ℤ} :

-a < b → -b < a

source

theorem int.sub_nonneg_of_le {a b : ℤ} :

b ≤ a → 0 ≤ a - b

source

theorem int.le_of_sub_nonneg {a b : ℤ} :

0 ≤ a - b → b ≤ a

source

theorem int.sub_nonpos_of_le {a b : ℤ} :

a ≤ b → a - b ≤ 0

source

theorem int.le_of_sub_nonpos {a b : ℤ} :

a - b ≤ 0 → a ≤ b

source

theorem int.sub_pos_of_lt {a b : ℤ} :

b < a → 0 < a - b

source

theorem int.lt_of_sub_pos {a b : ℤ} :

0 < a - b → b < a

source

theorem int.sub_neg_of_lt {a b : ℤ} :

a < b → a - b < 0

source

theorem int.lt_of_sub_neg {a b : ℤ} :

a - b < 0 → a < b

source

theorem int.add_le_of_le_neg_add {a b c : ℤ} :

b ≤ -a + c → a + b ≤ c

source

theorem int.le_neg_add_of_add_le {a b c : ℤ} :

a + b ≤ c → b ≤ -a + c

source

theorem int.add_le_of_le_sub_left {a b c : ℤ} :

b ≤ c - a → a + b ≤ c

source

theorem int.le_sub_left_of_add_le {a b c : ℤ} :

a + b ≤ c → b ≤ c - a

source

theorem int.add_le_of_le_sub_right {a b c : ℤ} :

a ≤ c - b → a + b ≤ c

source

theorem int.le_sub_right_of_add_le {a b c : ℤ} :

a + b ≤ c → a ≤ c - b

source

theorem int.le_add_of_neg_add_le {a b c : ℤ} :

-b + a ≤ c → a ≤ b + c

source

theorem int.neg_add_le_of_le_add {a b c : ℤ} :

a ≤ b + c → -b + a ≤ c

source

theorem int.le_add_of_sub_left_le {a b c : ℤ} :

a - b ≤ c → a ≤ b + c

source

theorem int.sub_left_le_of_le_add {a b c : ℤ} :

a ≤ b + c → a - b ≤ c

source

theorem int.le_add_of_sub_right_le {a b c : ℤ} :

a - c ≤ b → a ≤ b + c

source

theorem int.sub_right_le_of_le_add {a b c : ℤ} :

a ≤ b + c → a - c ≤ b

source

theorem int.le_add_of_neg_add_le_left {a b c : ℤ} :

-b + a ≤ c → a ≤ b + c

source

theorem int.neg_add_le_left_of_le_add {a b c : ℤ} :

a ≤ b + c → -b + a ≤ c

source

theorem int.le_add_of_neg_add_le_right {a b c : ℤ} :

-c + a ≤ b → a ≤ b + c

source

theorem int.neg_add_le_right_of_le_add {a b c : ℤ} :

a ≤ b + c → -c + a ≤ b

source

theorem int.le_add_of_neg_le_sub_left {a b c : ℤ} :

-a ≤ b - c → c ≤ a + b

source

theorem int.neg_le_sub_left_of_le_add {a b c : ℤ} :

c ≤ a + b → -a ≤ b - c

source

theorem int.le_add_of_neg_le_sub_right {a b c : ℤ} :

-b ≤ a - c → c ≤ a + b

source

theorem int.neg_le_sub_right_of_le_add {a b c : ℤ} :

c ≤ a + b → -b ≤ a - c

source

theorem int.sub_le_of_sub_le {a b c : ℤ} :

a - b ≤ c → a - c ≤ b

source

theorem int.sub_le_sub_left {a b : ℤ} (h : a ≤ b) (c : ℤ) :

c - b ≤ c - a

source

theorem int.sub_le_sub_right {a b : ℤ} (h : a ≤ b) (c : ℤ) :

a - c ≤ b - c

source

theorem int.sub_le_sub {a b c d : ℤ} :

a ≤ b → c ≤ d → a - d ≤ b - c

source

theorem int.add_lt_of_lt_neg_add {a b c : ℤ} :

b < -a + c → a + b < c

source

theorem int.lt_neg_add_of_add_lt {a b c : ℤ} :

a + b < c → b < -a + c

source

theorem int.add_lt_of_lt_sub_left {a b c : ℤ} :

b < c - a → a + b < c

source

theorem int.lt_sub_left_of_add_lt {a b c : ℤ} :

a + b < c → b < c - a

source

theorem int.add_lt_of_lt_sub_right {a b c : ℤ} :

a < c - b → a + b < c

source

theorem int.lt_sub_right_of_add_lt {a b c : ℤ} :

a + b < c → a < c - b

source

theorem int.lt_add_of_neg_add_lt {a b c : ℤ} :

-b + a < c → a < b + c

source

theorem int.neg_add_lt_of_lt_add {a b c : ℤ} :

a < b + c → -b + a < c

source

theorem int.lt_add_of_sub_left_lt {a b c : ℤ} :

a - b < c → a < b + c

source

theorem int.sub_left_lt_of_lt_add {a b c : ℤ} :

a < b + c → a - b < c

source

theorem int.lt_add_of_sub_right_lt {a b c : ℤ} :

a - c < b → a < b + c

source

theorem int.sub_right_lt_of_lt_add {a b c : ℤ} :

a < b + c → a - c < b

source

theorem int.lt_add_of_neg_add_lt_left {a b c : ℤ} :

-b + a < c → a < b + c

source

theorem int.neg_add_lt_left_of_lt_add {a b c : ℤ} :

a < b + c → -b + a < c

source

theorem int.lt_add_of_neg_add_lt_right {a b c : ℤ} :

-c + a < b → a < b + c

source

theorem int.neg_add_lt_right_of_lt_add {a b c : ℤ} :

a < b + c → -c + a < b

source

theorem int.lt_add_of_neg_lt_sub_left {a b c : ℤ} :

-a < b - c → c < a + b

source

theorem int.neg_lt_sub_left_of_lt_add {a b c : ℤ} :

c < a + b → -a < b - c

source

theorem int.lt_add_of_neg_lt_sub_right {a b c : ℤ} :

-b < a - c → c < a + b

source

theorem int.neg_lt_sub_right_of_lt_add {a b c : ℤ} :

c < a + b → -b < a - c

source

theorem int.sub_lt_of_sub_lt {a b c : ℤ} :

a - b < c → a - c < b

source

theorem int.sub_lt_sub_left {a b : ℤ} (h : a < b) (c : ℤ) :

c - b < c - a

source

theorem int.sub_lt_sub_right {a b : ℤ} (h : a < b) (c : ℤ) :

a - c < b - c

source

theorem int.sub_lt_sub {a b c d : ℤ} :

a < b → c < d → a - d < b - c

source

theorem int.sub_lt_sub_of_le_of_lt {a b c d : ℤ} :

a ≤ b → c < d → a - d < b - c

source

theorem int.sub_lt_sub_of_lt_of_le {a b c d : ℤ} :

a < b → c ≤ d → a - d < b - c

source

theorem int.sub_le_self (a : ℤ) {b : ℤ} :

b ≥ 0 → a - b ≤ a

source

theorem int.sub_lt_self (a : ℤ) {b : ℤ} :

b > 0 → a - b < a

source

theorem int.add_le_add_three {a b c d e f : ℤ} :

a ≤ d → b ≤ e → c ≤ f → a + b + c ≤ d + e + f

source

theorem int.mul_lt_mul_of_pos_left {a b c : ℤ} :

a < b → 0 < c → c * a < c * b

source

theorem int.mul_lt_mul_of_pos_right {a b c : ℤ} :

a < b → 0 < c → a * c < b * c

source

theorem int.mul_le_mul_of_nonneg_left {a b c : ℤ} :

a ≤ b → 0 ≤ c → c * a ≤ c * b

source

theorem int.mul_le_mul_of_nonneg_right {a b c : ℤ} :

a ≤ b → 0 ≤ c → a * c ≤ b * c

source

theorem int.mul_le_mul {a b c d : ℤ} :

a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d

source

theorem int.mul_nonpos_of_nonneg_of_nonpos {a b : ℤ} :

a ≥ 0 → b ≤ 0 → a * b ≤ 0

source

theorem int.mul_nonpos_of_nonpos_of_nonneg {a b : ℤ} :

a ≤ 0 → b ≥ 0 → a * b ≤ 0

source

theorem int.mul_lt_mul {a b c d : ℤ} :

a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d

source

theorem int.mul_lt_mul' {a b c d : ℤ} :

a ≤ c → b < d → b ≥ 0 → c > 0 → a * b < c * d

source

theorem int.mul_neg_of_pos_of_neg {a b : ℤ} :

a > 0 → b < 0 → a * b < 0

source

theorem int.mul_neg_of_neg_of_pos {a b : ℤ} :

a < 0 → b > 0 → a * b < 0

source

theorem int.mul_le_mul_of_nonpos_right {a b c : ℤ} :

b ≤ a → c ≤ 0 → a * c ≤ b * c

source

theorem int.mul_nonneg_of_nonpos_of_nonpos {a b : ℤ} :

a ≤ 0 → b ≤ 0 → 0 ≤ a * b

source

theorem int.mul_lt_mul_of_neg_left {a b c : ℤ} :

b < a → c < 0 → c * a < c * b

source

theorem int.mul_lt_mul_of_neg_right {a b c : ℤ} :

b < a → c < 0 → a * c < b * c

source

theorem int.mul_pos_of_neg_of_neg {a b : ℤ} :

a < 0 → b < 0 → 0 < a * b

source

theorem int.mul_self_le_mul_self {a b : ℤ} :

0 ≤ a → a ≤ b → a * a ≤ b * b

source

theorem int.mul_self_lt_mul_self {a b : ℤ} :

0 ≤ a → a < b → a * a < b * b

source

theorem int.of_nat_nonneg (n : ℕ) :

0 ≤ int.of_nat n

source

theorem int.coe_succ_pos (n : ℕ) :

↑(n.succ) > 0

source

theorem int.exists_eq_neg_of_nat {a : ℤ} :

a ≤ 0 → (∃ (n : ℕ), a = -↑n)

source

theorem int.nat_abs_of_nonneg {a : ℤ} :

a ≥ 0 → ↑(a.nat_abs) = a

source

theorem int.of_nat_nat_abs_of_nonpos {a : ℤ} :

a ≤ 0 → ↑(a.nat_abs) = -a

source

theorem int.lt_of_add_one_le {a b : ℤ} :

a + 1 ≤ b → a < b

source

theorem int.add_one_le_of_lt {a b : ℤ} :

a < b → a + 1 ≤ b

source

theorem int.lt_add_one_of_le {a b : ℤ} :

a ≤ b → a < b + 1

source

theorem int.le_of_lt_add_one {a b : ℤ} :

a < b + 1 → a ≤ b

source

theorem int.sub_one_le_of_lt {a b : ℤ} :

a ≤ b → a - 1 < b

source

theorem int.lt_of_sub_one_le {a b : ℤ} :

a - 1 < b → a ≤ b

source

theorem int.le_sub_one_of_lt {a b : ℤ} :

a < b → a ≤ b - 1

source

theorem int.lt_of_le_sub_one {a b : ℤ} :

a ≤ b - 1 → a < b

source

theorem int.sign_of_succ (n : ℕ) :

↑(n.succ).sign = 1

source

theorem int.sign_eq_one_of_pos {a : ℤ} :

0 < a → a.sign = 1

source

theorem int.sign_eq_neg_one_of_neg {a : ℤ} :

a < 0 → a.sign = -1

source

theorem int.eq_zero_of_sign_eq_zero {a : ℤ} :

a.sign = 0 → a = 0

source

theorem int.pos_of_sign_eq_one {a : ℤ} :

a.sign = 1 → 0 < a

source

theorem int.neg_of_sign_eq_neg_one {a : ℤ} :

a.sign = -1 → a < 0

source

theorem int.sign_eq_one_iff_pos (a : ℤ) :

a.sign = 1 ↔ 0 < a

source

theorem int.sign_eq_neg_one_iff_neg (a : ℤ) :

a.sign = -1 ↔ a < 0

source

theorem int.sign_eq_zero_iff_zero (a : ℤ) :

a.sign = 0 ↔ a = 0

source

theorem int.eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} :

a * b = 0 → a = 0 ∨ b = 0

source

theorem int.eq_of_mul_eq_mul_right {a b c : ℤ} :

a ≠ 0 → b * a = c * a → b = c

source

theorem int.eq_of_mul_eq_mul_left {a b c : ℤ} :

a ≠ 0 → a * b = a * c → b = c

source

theorem int.eq_one_of_mul_eq_self_left {a b : ℤ} :

a ≠ 0 → b * a = a → b = 1

source

theorem int.eq_one_of_mul_eq_self_right {a b : ℤ} :

b ≠ 0 → b * a = b → a = 1

mathlib documentation

core.init.data.int.order

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​int.​order

General documentation

Additional documentation

Library

core.init.data.int.order