Nuprl Lemma : matrix-plus-sq-real-matrix-add
∀[A,B:Top]. (A + B ~ A + B)
Proof
Definitions occuring in Statement :
real-matrix-add: A + B,
real-ring: real-ring(),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t,
matrix-plus: M + N
Definitions unfolded in proof :
real-matrix-add: A + B,
matrix-plus: M + N,
real-ring: real-ring(),
rng_plus: +r,
pi2: snd(t),
pi1: fst(t),
infix_ap: x f y,
matrix-ap: M[i,j],
mx: matrix(M[x; y]),
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation_alt,
introduction,
cut,
axiomSqEquality,
inhabitedIsType,
hypothesisEquality,
sqequalHypSubstitution,
isect_memberEquality_alt,
isectElimination,
thin,
isectIsTypeImplies,
extract_by_obid,
hypothesis
Latex:
\mforall{}[A,B:Top]. (A + B \msim{} A + B)
Date html generated:
2019_10_30-AM-08_18_24
Last ObjectModification:
2019_09_19-AM-11_53_38
Theory : reals
Home
Index