### Nuprl Lemma : rng_before_imp_before_all

`∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.`
`  ((↑before(k;map(λz.(fst(z));ps))) `` (↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). (x <b k))))`

Proof

Definitions occuring in Statement :  omralist: `omral(g;r)` before: `before(u;ps)` ball: ball map: `map(f;as)` assert: `↑b` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` lambda: `λx.A[x]` cdrng: `CDRng` grp_blt: `a <b b` oset_of_ocmon: `g↓oset` ocmon: `OCMon` grp_car: `|g|` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` ocmon: `OCMon` omon: `OMon` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` abmonoid: `AbMon` mon: `Mon` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff` infix_ap: `x f y` so_apply: `x[s]` cand: `A c∧ B` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` set_car: `|p|` pi1: `fst(t)` omralist: `omral(g;r)` grp_blt: `a <b b`
Lemmas referenced :  before_imp_before_all oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf cdrng_wf ocmon_wf cdrng_is_abdmonoid
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k:|g|.  \mforall{}ps:|omral(g;r)|.
((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (x  <\msubb{}  k))))

Date html generated: 2017_10_01-AM-10_04_58
Last ObjectModification: 2017_03_03-PM-01_09_49

Theory : polynom_3

Home Index