Nuprl Lemma : grp_op_preserves_le
∀[g:OCMon]. ∀[x,y,z:|g|]. (x * y) ≤ (x * z) supposing y ≤ z
Proof
Definitions occuring in Statement :
grp_leq: a ≤ b,
ocmon: OCMon,
grp_op: *,
grp_car: |g|,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
infix_ap: x f y
Definitions unfolded in proof :
monot: monot(T;x,y.R[x; y];f),
grp_leq: a ≤ b,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
infix_ap: x f y,
ocmon: OCMon,
abmonoid: AbMon,
mon: Mon,
implies: P ⇒ Q,
prop: ℙ,
guard: {T},
all: ∀x:A. B[x]
Lemmas referenced :
ocmon_6,
assert_witness,
grp_le_wf,
grp_op_wf,
grp_leq_wf,
grp_car_wf,
ocmon_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
sqequalSubstitution,
isect_memberFormation,
introduction,
isectElimination,
thin,
applyEquality,
setElimination,
rename,
hypothesisEquality,
hypothesis,
independent_functionElimination,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination
Latex:
\mforall{}[g:OCMon]. \mforall{}[x,y,z:|g|]. (x * y) \mleq{} (x * z) supposing y \mleq{} z
Date html generated:
2016_05_15-PM-00_12_46
Last ObjectModification:
2015_12_26-PM-11_42_13
Theory : groups_1
Home
Index