### Nuprl Lemma : continuous-rdiv

`∀I:Interval. ∀f,g:I ⟶ℝ.`
`  (f[x] continuous for x ∈ I `` g[x] continuous for x ∈ I `` g[x]≠r0 for x ∈ I `` (f[x]/g[x]) continuous for x ∈ I)`

Proof

Definitions occuring in Statement :  nonzero-on: `f[x]≠r0 for x ∈ I` continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` interval: `Interval` rdiv: `(x/y)` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` uimplies: `b supposing a` rneq: `x ≠ y` sq_stable: `SqStable(P)` squash: `↓T` rfun-eq: `rfun-eq(I;f;g)` r-ap: `f(x)` false: `False` not: `¬A` rat_term_to_real: `rat_term_to_real(f;t)` rtermDivide: `num "/" denom` rat_term_ind: rat_term_ind rtermVar: `rtermVar(var)` pi1: `fst(t)` and: `P ∧ Q` true: `True` rtermMultiply: `left "*" right` rtermConstant: `"const"` pi2: `snd(t)` label: `...\$L... t` prop: `ℙ`
Lemmas referenced :  nonzero-on-implies continuous_functionality_wrt_rfun-eq rmul_wf rdiv_wf int-to-real_wf sq_stable__i-member assert-rat-term-eq2 rtermMultiply_wf rtermVar_wf rtermDivide_wf rtermConstant_wf istype-int nonzero-on_wf real_wf i-member_wf continuous_wf rfun_wf interval_wf continuous-mul continuous-rinv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis because_Cache isectElimination sqequalRule lambdaEquality_alt applyEquality closedConclusion natural_numberEquality independent_isectElimination setElimination rename imageMemberEquality baseClosed imageElimination int_eqEquality approximateComputation independent_pairFormation universeIsType setIsType inhabitedIsType

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
(f[x]  continuous  for  x  \mmember{}  I
{}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I
{}\mRightarrow{}  g[x]\mneq{}r0  for  x  \mmember{}  I
{}\mRightarrow{}  (f[x]/g[x])  continuous  for  x  \mmember{}  I)

Date html generated: 2019_10_30-AM-07_46_48
Last ObjectModification: 2019_04_03-AM-00_22_24

Theory : reals

Home Index