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