Nuprl Lemma : decreasing-on-interval_wf

[I:Interval]. ∀[f:I ⟶ℝ].  (f[x] decreasing for x ∈ I ∈ ℙ)


Proof




Definitions occuring in Statement :  decreasing-on-interval: f[x] decreasing for x ∈ I rfun: I ⟶ℝ interval: Interval uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T decreasing-on-interval: f[x] decreasing for x ∈ I prop: so_lambda: λ2x.t[x] all: x:A. B[x] implies:  Q so_apply: x[s] rfun: I ⟶ℝ
Lemmas referenced :  all_wf real_wf i-member_wf rless_wf rleq_wf rfun_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesis hypothesisEquality lambdaEquality lambdaFormation setElimination rename because_Cache functionEquality applyEquality dependent_set_memberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    (f[x]  decreasing  for  x  \mmember{}  I  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-10_18_54
Last ObjectModification: 2015_12_27-PM-10_56_59

Theory : reals


Home Index