### Nuprl Lemma : continuous-abs-subtype

`∀[I:Interval]. ∀[f:I ⟶ℝ].  (f[x] continuous for x ∈ I ⊆r |f[x]| continuous for x ∈ I)`

Proof

Definitions occuring in Statement :  continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` interval: `Interval` rabs: `|x|` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` label: `...\$L... t` rfun: `I ⟶ℝ` so_apply: `x[s]` prop: `ℙ` continuous-abs-ext implies: `P `` Q` all: `∀x:A. B[x]` continuous: `f[x] continuous for x ∈ I` sq_exists: `∃x:{A| B[x]}` and: `P ∧ Q` nat_plus: `ℕ+` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rless: `x < y` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` squash: `↓T` true: `True` sq_stable: `SqStable(P)` rleq: `x ≤ y` rnonneg: `rnonneg(x)` le: `A ≤ B`
Lemmas referenced :  continuous_wf i-member_wf real_wf rfun_wf interval_wf continuous-abs-ext isect_wf rabs_wf equal_wf nat_plus_wf set_wf icompact_wf i-approx_wf rless_wf int-to-real_wf less_than_wf rleq_wf rsub_wf i-member-approx rdiv_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf squash_wf true_wf iff_weakening_equal subtype_rel_dep_function rmin_wf rmin-idempotent-eq sq_exists_wf less_than'_wf sq_stable__and sq_stable__rless sq_stable__all sq_stable__rleq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality rename extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality setElimination dependent_set_memberEquality hypothesis setEquality axiomEquality isect_memberEquality because_Cache instantiate equalityTransitivity equalitySymmetry functionEquality lambdaFormation dependent_functionElimination independent_functionElimination isectEquality functionExtensionality productEquality natural_numberEquality independent_isectElimination inrFormation productElimination unionElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination universeEquality imageMemberEquality baseClosed hyp_replacement applyLambdaEquality minusEquality independent_pairEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    (f[x]  continuous  for  x  \mmember{}  I  \msubseteq{}r  |f[x]|  continuous  for  x  \mmember{}  I)

Date html generated: 2017_10_03-AM-10_23_04
Last ObjectModification: 2017_07_28-AM-08_07_28

Theory : reals

Home Index