Nuprl Lemma : upper-bounds_wf
∀[A:Set(ℝ)]. (upper-bounds(A) ∈ Set(ℝ))
Proof
Definitions occuring in Statement :
upper-bounds: upper-bounds(A),
rset: Set(ℝ),
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
upper-bounds: upper-bounds(A),
rset: Set(ℝ),
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
upper-bound: A ≤ b,
guard: {T},
uimplies: b supposing a
Lemmas referenced :
upper-bound_wf,
all_wf,
real_wf,
req_wf,
rleq_transitivity,
rleq_weakening,
rset-member_wf,
set_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
introduction,
cut,
setElimination,
thin,
rename,
dependent_set_memberEquality,
lambdaEquality,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
hypothesisEquality,
functionEquality,
applyEquality,
because_Cache,
lambdaFormation,
dependent_functionElimination,
independent_functionElimination,
independent_isectElimination,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
instantiate,
cumulativity,
universeEquality
Latex:
\mforall{}[A:Set(\mBbbR{})]. (upper-bounds(A) \mmember{} Set(\mBbbR{}))
Date html generated:
2016_05_18-AM-08_11_25
Last ObjectModification:
2015_12_28-AM-01_17_00
Theory : reals
Home
Index