### Nuprl Lemma : rng_before_all_imp_before

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

Proof

Definitions occuring in Statement :  before: `before(u;ps)` ball: ball map: `map(f;as)` list: `T List` assert: `↑b` pi1: `fst(t)` all: `∀x:A. B[x]` implies: `P `` Q` lambda: `λx.A[x]` product: `x:A × B[x]` crng: `CRng` rng_car: `|r|` grp_blt: `a <b b` oset_of_ocmon: `g↓oset` ocmon: `OCMon` grp_car: `|g|`
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` crng: `CRng` abgrp: `AbGrp` grp: `Group{i}` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` set_car: `|p|` pi1: `fst(t)` add_grp_of_rng: `r↓+gp` grp_car: `|g|` grp_blt: `a <b b`
Lemmas referenced :  before_all_imp_before 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 add_grp_of_rng_wf_b mon_wf inverse_wf grp_id_wf grp_inv_wf comm_wf set_wf crng_wf ocmon_wf
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:CRng.  \mforall{}k:|g|.  \mforall{}ps:(|g|  \mtimes{}  |r|)  List.
((\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (x  <\msubb{}  k)))  {}\mRightarrow{}  (\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps))))

Date html generated: 2017_10_01-AM-10_04_59
Last ObjectModification: 2017_03_03-PM-01_09_28

Theory : polynom_3

Home Index