Nuprl Lemma : maps-compact_wf

[I,J:Interval]. ∀[f:I ⟶ℝ].  (maps-compact(I;J;x.f[x]) ∈ ℙ)


Proof




Definitions occuring in Statement :  maps-compact: maps-compact(I;J;x.f[x]) 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 maps-compact: maps-compact(I;J;x.f[x]) and: P ∧ Q prop: so_lambda: λ2x.t[x] all: x:A. B[x] so_apply: x[s] rfun: I ⟶ℝ implies:  Q
Lemmas referenced :  all_wf nat_plus_wf icompact_wf i-approx_wf iproper_wf exists_wf real_wf i-member_wf i-member-approx rfun_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesis productEquality hypothesisEquality because_Cache lambdaEquality lambdaFormation setElimination rename productElimination applyEquality dependent_functionElimination independent_functionElimination dependent_set_memberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I,J:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    (maps-compact(I;J;x.f[x])  \mmember{}  \mBbbP{})



Date html generated: 2016_10_26-AM-09_58_06
Last ObjectModification: 2016_08_24-PM-00_57_34

Theory : reals


Home Index