Nuprl Lemma : matrix-scalar-mul-sq-real-matrix-scalar-mul
∀[c,A:Top]. (c*A ~ c*A)
Proof
Definitions occuring in Statement :
real-matrix-scalar-mul: c*A,
real-ring: real-ring(),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t,
matrix-scalar-mul: k*M
Definitions unfolded in proof :
real-matrix-scalar-mul: c*A,
matrix-scalar-mul: k*M,
real-ring: real-ring(),
rng_times: *,
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{}[c,A:Top]. (c*A \msim{} c*A)
Date html generated:
2019_10_30-AM-08_20_07
Last ObjectModification:
2019_09_19-PM-00_02_01
Theory : reals
Home
Index