rainbow.math.or-foundation

Foundations src/rainbow/math/or_foundation.clj0 definitions, 1 theorems

Small reusable proof-data laws shared by OR representations.

function/product-diagonal-injective

TheoremFor all inputsNo axiomsSource, line 31

function/product-diagonal-injective.{u} :
  (A : Type u) (left right : A)
  (same-image : (fun value => data/pair A A value value) left = (fun value => data/pair A A value value) right)
  → left = right

= = equality/Eq