Nuprl Lemma : superlevelset_wf

[I:Interval]. ∀[f:I ⟶ℝ]. ∀[c:ℝ].  (superlevelset(I;f;c) ∈ ℝ ⟶ ℙ)


Proof




Definitions occuring in Statement :  superlevelset: superlevelset(I;f;c) rfun: I ⟶ℝ interval: Interval real: uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T superlevelset: superlevelset(I;f;c) prop: and: P ∧ Q uimplies: supposing a
Lemmas referenced :  i-member_wf rleq_wf r-ap_wf real_wf rfun_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[c:\mBbbR{}].    (superlevelset(I;f;c)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2016_05_18-AM-08_51_18
Last ObjectModification: 2015_12_27-PM-11_43_01

Theory : reals


Home Index