Nuprl Lemma : imax-list-lb
∀[L:ℤ List]. ∀[a:ℤ]. uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||
Proof
Definitions occuring in Statement :
imax-list: imax-list(L),
l_all: (∀x∈L.P[x]),
length: ||as||,
list: T List,
less_than: a < b,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
le: A ≤ B,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
assoc: Assoc(T;op),
uall: ∀[x:A]. B[x],
member: t ∈ T,
infix_ap: x f y,
uimplies: b supposing a,
all: ∀x:A. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
guard: {T},
prop: ℙ,
rev_implies: P ⇐ Q,
cand: A c∧ B,
imax-list: imax-list(L),
uiff: uiff(P;Q),
l_all: (∀x∈L.P[x]),
le: A ≤ B,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
imax_assoc,
istype-int,
combine-list-rel-and,
imax_wf,
le_wf,
iff_weakening_uiff,
imax_lb,
le_witness_for_triv,
imax-list_wf,
l_all_wf,
l_member_wf,
less_than_wf,
length_wf,
list_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
Error :inhabitedIsType,
Error :isect_memberEquality_alt,
axiomEquality,
intEquality,
dependent_functionElimination,
Error :lambdaEquality_alt,
because_Cache,
independent_functionElimination,
Error :lambdaFormation_alt,
independent_pairFormation,
productElimination,
Error :universeIsType,
productEquality,
Error :productIsType,
promote_hyp,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
Error :functionIsTypeImplies,
setElimination,
rename,
Error :setIsType,
independent_pairEquality,
natural_numberEquality
Latex:
\mforall{}[L:\mBbbZ{} List]. \mforall{}[a:\mBbbZ{}]. uiff(imax-list(L) \mleq{} a;(\mforall{}b\mmember{}L.b \mleq{} a)) supposing 0 < ||L||
Date html generated:
2019_06_20-PM-01_19_38
Last ObjectModification:
2018_10_07-AM-00_02_43
Theory : list_1
Home
Index