Nuprl Lemma : rmin-idempotent-eq
∀[x:ℝ]. (rmin(x;x) = x ∈ ℝ)
Proof
Definitions occuring in Statement :
rmin: rmin(x;y),
real: ℝ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
real: ℝ,
member: t ∈ T,
nat_plus: ℕ+,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
prop: ℙ,
rmin: rmin(x;y),
implies: P ⇒ Q,
all: ∀x:A. B[x],
top: Top,
not: ¬A,
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
or: P ∨ Q,
decidable: Dec(P),
uimplies: b supposing a,
uiff: uiff(P;Q)
Lemmas referenced :
real-regular,
less_than_wf,
regular-int-seq_wf,
real_wf,
nat_plus_wf,
equal_wf,
int_formula_prop_wf,
int_term_value_var_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
itermVar_wf,
intformle_wf,
intformnot_wf,
satisfiable-full-omega-tt,
decidable__le,
nat_plus_properties,
le-iff-imin
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
equalitySymmetry,
dependent_set_memberEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
natural_numberEquality,
sqequalRule,
independent_pairFormation,
imageMemberEquality,
baseClosed,
hypothesis,
functionExtensionality,
independent_functionElimination,
dependent_functionElimination,
equalityTransitivity,
lambdaFormation,
intEquality,
rename,
setElimination,
applyEquality,
computeAll,
voidEquality,
voidElimination,
isect_memberEquality,
int_eqEquality,
lambdaEquality,
dependent_pairFormation,
unionElimination,
independent_isectElimination,
productElimination,
because_Cache
Latex:
\mforall{}[x:\mBbbR{}]. (rmin(x;x) = x)
Date html generated:
2017_10_03-AM-08_33_30
Last ObjectModification:
2017_09_20-PM-05_36_25
Theory : reals
Home
Index