Reference · Foundations

rainbow.math.checks

Foundationssrc/rainbow/math/checks.clj0 definitions, 12 theorems

General lemmas: checks. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.nat.infinitemath.rational.nnrat.identitiesmath.nat.at-most-cancellationmath.rational.nnrat.order-equivalencemath.rational.nnrat.archimedeanmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociationmath.rational.signed.order-transitivitymath.rational.signed.convergencemath.rational.signed.order-respectsmath.rational.signed.limit-uniquenessmath.rational.signed.strict-ordermath.rational.signed.multiplymath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.ringmath.rational.nnrat.multiply-monotonemath.rational.nnrat.order-differencemath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.minmaxmath.rational.nnrat.farkas-elim-listmath.rational.signed.no-zero-divisorsmath.rational.signed.decide-ordermath.rational.signed.decide-reflexivemath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.rational.signed.unit-lawsmath.nat.strict-below-splitmath.nat.strict-below-moremath.rational.signed.clampmath.rational.signed.distancemath.nat.linear-ordermath.rational.signed.structural-equality

signed/all-at-most-value :
  (x₁ x₂ : ℕ → ℚ) (x₃ : ℕ)
  → ℚ

signed/expr-sum-value :
  (x₁ : ℕ → ℚ) (x₂ : ℕ)
  → ℚ

signed/one-not-at-most-zero :
  (h₁ : 1 ≤ 0)
  → proposition/falsity

signed/all-at-most-sound :
  (A B : ℕ → ℚ) (k : ℕ)
  (h : signed/all-at-most-value A B k = 1)
  (i : ℕ) (hi : nat/strict-below i k)
  → A i ≤ B i

signed/all-at-most-complete :
  (A B : ℕ → ℚ) (k : ℕ)
  (h : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), A i ≤ B i)
  → signed/all-at-most-value A B k = 1

signed/all-at-most-zero-or-one :
  (A B : ℕ → ℚ) (k : ℕ)
  → proposition/disjunction (signed/all-at-most-value A B k = 0) (signed/all-at-most-value A B k = 1)

signed/all-at-most-one-of-at-least-one :
  (A B : ℕ → ℚ) (k : ℕ)
  (h : 1 ≤ signed/all-at-most-value A B k)
  → signed/all-at-most-value A B k = 1

signed/both-sound :
  (P Q : ℚ)
  (h : data/Bool.rec (fun x₄ => ℚ) 0 Q (signed/decide-at-most 1 P) = 1)
  → proposition/conjunction (1 ≤ P) (Q = 1)

signed/both-complete :
  (P Q : ℚ)
  (hp : 1 ≤ P)
  (hq : Q = 1)
  → data/Bool.rec (fun x₄ => ℚ) 0 Q (signed/decide-at-most 1 P) = 1

signed/all-at-most-value-congruence :
  (A B A2 B2 : ℕ → ℚ)
  (HA : ∀ (i : ℕ), A i = A2 i)
  (HB : ∀ (i : ℕ), B i = B2 i)
  (k : ℕ)
  → signed/all-at-most-value A B k = signed/all-at-most-value A2 B2 k

signed/expr-sum-value-congruence :
  (G G2 : ℕ → ℚ)
  (H : ∀ (i : ℕ), G i = G2 i)
  (k : ℕ)
  → signed/expr-sum-value G k = signed/expr-sum-value G2 k

signed/expr-sum-value-congruence-below :
  (G G2 : ℕ → ℚ) (k : ℕ)
  (H : ∀ (a : ℕ), ∀ (ha : nat/strict-below a k), G a = G2 a)
  → signed/expr-sum-value G k = signed/expr-sum-value G2 k