Nuprl Lemma : maximal-in-list
∀[A:Type]. ∀f:A ⟶ ℤ. ∀L:A List. (∃a∈L. (∀x∈L.(f x) ≤ (f a))) supposing 0 < ||L||
Proof
Definitions occuring in Statement :
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
length: ||as||,
list: T List,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
le: A ≤ B,
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
implies: P ⇒ Q,
and: P ∧ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
exists: ∃x:A. B[x],
cand: A c∧ B,
sq_type: SQType(T)
Lemmas referenced :
list-max-property,
member-less_than,
length_wf,
istype-less_than,
list_wf,
istype-int,
istype-universe,
list-max_wf,
l_member_wf,
int_subtype_base,
l_all_wf,
le_wf,
l_exists_iff,
subtype_base_sq
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
Error :lambdaFormation_alt,
dependent_functionElimination,
natural_numberEquality,
independent_isectElimination,
rename,
Error :universeIsType,
Error :functionIsType,
instantiate,
universeEquality,
sqequalRule,
Error :lambdaEquality_alt,
applyEquality,
Error :inhabitedIsType,
productElimination,
Error :productIsType,
setElimination,
Error :equalityIstype,
because_Cache,
sqequalBase,
equalitySymmetry,
Error :setIsType,
equalityTransitivity,
independent_functionElimination,
Error :dependent_pairFormation_alt,
independent_pairFormation,
cumulativity,
intEquality
Latex:
\mforall{}[A:Type]. \mforall{}f:A {}\mrightarrow{} \mBbbZ{}. \mforall{}L:A List. (\mexists{}a\mmember{}L. (\mforall{}x\mmember{}L.(f x) \mleq{} (f a))) supposing 0 < ||L||
Date html generated:
2019_06_20-PM-01_30_56
Last ObjectModification:
2018_11_28-PM-03_24_31
Theory : list_1
Home
Index