Nuprl Lemma : imax-class-lb
∀[Info,T:Type]. ∀[f:T ⟶ ℤ]. ∀[es:EO+(Info)]. ∀[lb:ℤ]. ∀[X:EClass(T)]. ∀[e:E(X)]. ∀[n:ℤ].
uiff((maximum f[v] ≥ lb with v from X)(e) ≤ n;(∀[e':E(X)]. f[X(e')] ≤ n supposing e' ≤loc e ) ∧ (lb ≤ n))
Proof
Definitions occuring in Statement :
imax-class: (maximum f[v] ≥ lb with v from X),
es-E-interface: E(X),
eclass-val: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
le: A ≤ B,
and: P ∧ Q,
function: x:A ⟶ B[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
top: Top,
es-E-interface: E(X),
ge: i ≥ j ,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
implies: P ⇒ Q,
not: ¬A,
prop: ℙ,
so_lambda: λ2x.t[x],
iff: P ⇐⇒ Q,
le: A ≤ B,
sq_type: SQType(T),
guard: {T},
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
rev_implies: P ⇐ Q,
squash: ↓T,
eclass-vals: X(L),
compose: f o g,
l_all: (∀x∈L.P[x]),
int_seg: {i..j-},
lelt: i ≤ j < k,
less_than: a < b,
sq_stable: SqStable(P)
Latex:
\mforall{}[Info,T:Type]. \mforall{}[f:T {}\mrightarrow{} \mBbbZ{}]. \mforall{}[es:EO+(Info)]. \mforall{}[lb:\mBbbZ{}]. \mforall{}[X:EClass(T)]. \mforall{}[e:E(X)]. \mforall{}[n:\mBbbZ{}].
uiff((maximum f[v] \mgeq{} lb with v from X)(e) \mleq{} n;(\mforall{}[e':E(X)]. f[X(e')] \mleq{} n supposing e' \mleq{}loc e )
\mwedge{} (lb \mleq{} n))
Date html generated:
2016_05_17-AM-07_02_01
Last ObjectModification:
2016_01_17-PM-06_56_37
Theory : event-ordering
Home
Index