Documentation

Init.Omega.Int

Lemmas about Nat, Int, and Fin needed internally by omega. #

These statements are useful for constructing proof expressions, but unlikely to be widely useful, so are inside the Lean.Omega namespace.

If you do find a use for them, please move them into the appropriate file and namespace!

theorem Lean.Omega.Int.ofNat_pow (a : Nat) (b : Nat) :
(a ^ b) = a ^ b
theorem Lean.Omega.Int.pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) :
0 < a ^ b
theorem Lean.Omega.Int.ofNat_pos {a : Nat} :
0 < a 0 < a
theorem Lean.Omega.Int.ofNat_pos_of_pos {a : Nat} (h : 0 < a) :
0 < a
theorem Lean.Omega.Int.ofNat_lt_of_lt {x : Nat} {y : Nat} (h : x < y) :
x < y
theorem Lean.Omega.Int.ofNat_le_of_le {x : Nat} {y : Nat} (h : x y) :
x y
theorem Lean.Omega.Int.ofNat_shiftLeft_eq {x : Nat} {y : Nat} :
(x <<< y) = x * (2 ^ y)
theorem Lean.Omega.Int.ofNat_shiftRight_eq_div_pow {x : Nat} {y : Nat} :
(x >>> y) = x / (2 ^ y)
theorem Lean.Omega.Int.emod_ofNat_nonneg {x : Nat} {y : Int} :
0 x % y
theorem Lean.Omega.Int.lt_of_not_ge {x : Int} {y : Int} (h : ¬x y) :
y < x
theorem Lean.Omega.Int.lt_of_not_le {x : Int} {y : Int} (h : ¬x y) :
y < x
theorem Lean.Omega.Int.not_le_of_lt {x : Int} {y : Int} (h : y < x) :
¬x y
theorem Lean.Omega.Int.lt_le_asymm {x : Int} {y : Int} (h₁ : y < x) (h₂ : x y) :
theorem Lean.Omega.Int.le_lt_asymm {x : Int} {y : Int} (h₁ : y x) (h₂ : x < y) :
theorem Lean.Omega.Int.le_of_not_gt {x : Int} {y : Int} (h : ¬y > x) :
y x
theorem Lean.Omega.Int.not_lt_of_ge {x : Int} {y : Int} (h : y x) :
¬y < x
theorem Lean.Omega.Int.le_of_not_lt {x : Int} {y : Int} (h : ¬x < y) :
y x
theorem Lean.Omega.Int.not_lt_of_le {x : Int} {y : Int} (h : y x) :
¬x < y
theorem Lean.Omega.Int.add_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) :
a + c = b + d
theorem Lean.Omega.Int.mul_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) :
a * c = b * d
theorem Lean.Omega.Int.mul_congr_left {a : Int} {b : Int} (h₁ : a = b) (c : Int) :
a * c = b * c
theorem Lean.Omega.Int.sub_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) :
a - c = b - d
theorem Lean.Omega.Int.neg_congr {a : Int} {b : Int} (h₁ : a = b) :
-a = -b
theorem Lean.Omega.Int.lt_of_gt {x : Int} {y : Int} (h : x > y) :
y < x
theorem Lean.Omega.Int.le_of_ge {x : Int} {y : Int} (h : x y) :
y x
theorem Lean.Omega.Int.ofNat_mul_nonneg {a : Nat} {b : Nat} :
0 a * b
theorem Lean.Omega.Int.ofNat_sub_eq_zero {b : Nat} {a : Nat} (h : ¬b a) :
(a - b) = 0
theorem Lean.Omega.Int.ofNat_sub_dichotomy {a : Nat} {b : Nat} :
b a (a - b) = a - b a < b (a - b) = 0
theorem Lean.Omega.Int.ofNat_congr {a : Nat} {b : Nat} (h : a = b) :
a = b
theorem Lean.Omega.Int.ofNat_sub_sub {a : Nat} {b : Nat} {c : Nat} :
(a - b - c) = (a - (b + c))
theorem Lean.Omega.Int.ofNat_min (a : Nat) (b : Nat) :
(min a b) = min a b
theorem Lean.Omega.Int.ofNat_max (a : Nat) (b : Nat) :
(max a b) = max a b
theorem Lean.Omega.Int.ofNat_natAbs (a : Int) :
a.natAbs = if 0 a then a else -a
theorem Lean.Omega.Int.natAbs_dichotomy {a : Int} :
0 a a.natAbs = a a < 0 a.natAbs = -a
theorem Lean.Omega.Int.neg_le_natAbs {a : Int} :
-a a.natAbs
theorem Lean.Omega.Int.add_le_iff_le_sub {a : Int} {b : Int} {c : Int} :
a + b c a c - b
theorem Lean.Omega.Int.le_add_iff_sub_le {a : Int} {b : Int} {c : Int} :
a b + c a - c b
theorem Lean.Omega.Int.ofNat_fst_mk {β : Type u_1} {x : Nat} {y : β} :
(x, y).fst = x
theorem Lean.Omega.Int.ofNat_snd_mk {α : Type u_1} {x : α} {y : Nat} :
(x, y).snd = y
theorem Lean.Omega.Nat.lt_of_gt {x : Nat} {y : Nat} (h : x > y) :
y < x
theorem Lean.Omega.Nat.le_of_ge {x : Nat} {y : Nat} (h : x y) :
y x
theorem Lean.Omega.Fin.ne_iff_lt_or_gt {n : Nat} {i : Fin n} {j : Fin n} :
i j i < j i > j
theorem Lean.Omega.Fin.lt_or_gt_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
i < j i > j
theorem Lean.Omega.Fin.not_le {n : Nat} {i : Fin n} {j : Fin n} :
¬i j j < i
theorem Lean.Omega.Fin.not_lt {n : Nat} {i : Fin n} {j : Fin n} :
¬i < j j i
theorem Lean.Omega.Fin.lt_of_not_le {n : Nat} {i : Fin n} {j : Fin n} (h : ¬i j) :
j < i
theorem Lean.Omega.Fin.le_of_not_lt {n : Nat} {i : Fin n} {j : Fin n} (h : ¬i < j) :
j i
theorem Lean.Omega.Fin.ofNat_val_add {n : Nat} {x : Fin n} {y : Fin n} :
(x + y) = (x + y) % n
theorem Lean.Omega.Fin.ofNat_val_sub {n : Nat} {x : Fin n} {y : Fin n} :
(x - y) = ((n - y) + x) % n
theorem Lean.Omega.Fin.ofNat_val_mul {n : Nat} {x : Fin n} {y : Fin n} :
(x * y) = x * y % n
theorem Lean.Omega.Fin.ofNat_val_natCast {n : Nat} {x : Nat} {y : Nat} (h : y = x % (n + 1)) :
theorem Lean.Omega.Prod.of_lex :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp} {p q : α × β}, Prod.Lex r s p qr p.fst q.fst p.fst = q.fst s p.snd q.snd
theorem Lean.Omega.Prod.of_not_lex {α : Type u_1} {r : ααProp} [DecidableEq α] {β : Type u_2} {s : ββProp} {p : α × β} {q : α × β} (w : ¬Prod.Lex r s p q) :
¬r p.fst q.fst (p.fst q.fst ¬s p.snd q.snd)
theorem Lean.Omega.Prod.fst_mk :
∀ {α : Type u_1} {x : α} {β : Type u_2} {y : β}, (x, y).fst = x
theorem Lean.Omega.Prod.snd_mk :
∀ {α : Type u_1} {x : α} {α_1 : Type u_2} {y : α_1}, (x, y).snd = y