### Nuprl Lemma : continuous-rneq

`∀I:Interval. ∀f:I ⟶ℝ.  (f[x] continuous for x ∈ I `` (∀a,b:{x:ℝ| x ∈ I} .  (f[a] ≠ f[b] `` a ≠ b)))`

Proof

Definitions occuring in Statement :  continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` rneq: `x ≠ y` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} `
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` rfun: `I ⟶ℝ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ` exists: `∃x:A. B[x]` cand: `A c∧ B` sq_stable: `SqStable(P)` squash: `↓T` so_lambda: `λ2x.t[x]` label: `...\$L... t` rneq: `x ≠ y` or: `P ∨ Q` guard: `{T}` uimplies: `b supposing a` continuous: `f[x] continuous for x ∈ I` sq_exists: `∃x:{A| B[x]}` nat_plus: `ℕ+` rless: `x < y` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` subtype_rel: `A ⊆r B` rleq: `x ≤ y` rnonneg: `rnonneg(x)` le: `A ≤ B`
Lemmas referenced :  rneq-iff-rabs rless_irreflexivity rless_transitivity1 rleq_weakening_rless not-rless sq_stable__rleq sq_stable__all sq_stable__rless sq_stable__and squash_wf nat_plus_wf less_than'_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_plus_properties rless-int rdiv_wf i-member-approx rleq_wf all_wf i-approx_wf icompact_wf i-approx-compact req_weakening radd-zero-both rless_functionality or_wf radd_wf interval_wf rfun_wf continuous_wf i-member_wf real_wf set_wf rneq_wf sq_stable__i-member i-approx-containing2 rless_wf int-to-real_wf rabs-difference-lower-bound rsub_wf rabs_wf small-reciprocal-real
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality isectElimination applyEquality sqequalRule hypothesisEquality hypothesis natural_numberEquality productElimination independent_functionElimination setElimination rename introduction imageMemberEquality baseClosed imageElimination independent_pairFormation lambdaEquality setEquality unionElimination inrFormation inlFormation because_Cache addLevel orFunctionality independent_isectElimination isect_memberEquality functionEquality dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality computeAll minusEquality independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (f[a]  \mneq{}  f[b]  {}\mRightarrow{}  a  \mneq{}  b)))

Date html generated: 2016_05_18-AM-09_08_58
Last ObjectModification: 2016_01_17-AM-02_37_40

Theory : reals

Home Index