### Nuprl Lemma : real-has-value

`∀[x:ℝ]. (x)↓`

Proof

Definitions occuring in Statement :  real: `ℝ` has-value: `(a)↓` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` real: `ℝ` has-value: `(a)↓` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` exists: `∃x:A. B[x]` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` and: `P ∧ Q` prop: `ℙ`
Lemmas referenced :  value-type-has-value value-type_wf int-value-type less_than_wf nat_plus_wf function-value-type real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename sqequalRule axiomSqleEquality hypothesis lemma_by_obid isectElimination lambdaEquality intEquality independent_isectElimination dependent_pairFormation dependent_set_memberEquality natural_numberEquality independent_pairFormation imageMemberEquality hypothesisEquality baseClosed functionEquality

Latex:
\mforall{}[x:\mBbbR{}].  (x)\mdownarrow{}

Date html generated: 2016_05_18-AM-06_46_57
Last ObjectModification: 2016_01_17-AM-01_45_20

Theory : reals

Home Index