Nuprl Lemma : real-det-sq-matrix-det
∀n:ℕ. ∀M:Top. (|M| ~ |M|)
Proof
Definitions occuring in Statement :
real-det: |M|,
real-ring: real-ring(),
nat: ℕ,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t,
matrix-det: |M|
Definitions unfolded in proof :
all: ∀x:A. B[x],
real-det: |M|,
matrix-det: |M|,
real-ring: real-ring(),
rng_minus: -r,
pi2: snd(t),
pi1: fst(t),
matrix-ap: M[i,j],
rng_prod: rng_prod,
rng_lsum: Σ{r} x ∈ as. f[x],
rng_plus: +r,
rng_zero: 0,
mon_itop: Π lb ≤ i < ub. E[i],
mul_mon_of_rng: r↓xmn,
grp_op: *,
grp_id: e,
rng_times: *,
rng_one: 1,
r-list-sum: r-list-sum(L),
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat: ℕ,
so_lambda: λ2x.t[x],
top: Top,
so_apply: x[s]
Lemmas referenced :
rprod-as-itop,
istype-void,
istype-top,
istype-nat
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
setElimination,
rename,
hypothesisEquality,
hypothesis,
isect_memberEquality_alt,
voidElimination
Latex:
\mforall{}n:\mBbbN{}. \mforall{}M:Top. (|M| \msim{} |M|)
Date html generated:
2019_10_30-AM-08_21_27
Last ObjectModification:
2019_09_18-PM-05_55_32
Theory : reals
Home
Index