Nuprl Lemma : ball_functionality_wrt_permr
∀T:Type. ∀as,bs:T List. ∀P,Q:T ⟶ 𝔹. ((as ≡(T) bs) ⇒ (∀x:T. P[x] = Q[x]) ⇒ ∀bx(:T) ∈ as. P[x] = ∀bx(:T) ∈ bs. Q[x])
Proof
Definitions occuring in Statement :
ball: ball,
permr: as ≡(T) bs,
list: T List,
bool: 𝔹,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
ball: ball,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_apply: x[s],
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
true: True,
squash: ↓T,
bool: 𝔹,
grp_car: |g|,
pi1: fst(t),
band_mon: <𝔹,∧b>,
guard: {T},
uimplies: b supposing a,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
istype-universe,
bool_wf,
permr_wf,
list_wf,
band_mon_wf,
abmonoid_subtype_iabmonoid,
mem_f_wf,
mon_for_wf,
equal_wf,
squash_wf,
true_wf,
mon_for_functionality_wrt_permr,
subtype_rel_self,
grp_car_wf,
mon_subtype_grp_sig,
abmonoid_subtype_mon,
subtype_rel_transitivity,
abmonoid_wf,
mon_wf,
grp_sig_wf,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
hypothesis,
sqequalRule,
functionIsType,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
equalityIsType1,
universeIsType,
applyEquality,
dependent_functionElimination,
inhabitedIsType,
universeEquality,
lambdaEquality_alt,
because_Cache,
natural_numberEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
instantiate,
independent_isectElimination,
imageMemberEquality,
baseClosed,
productElimination
Latex:
\mforall{}T:Type. \mforall{}as,bs:T List. \mforall{}P,Q:T {}\mrightarrow{} \mBbbB{}.
((as \mequiv{}(T) bs) {}\mRightarrow{} (\mforall{}x:T. P[x] = Q[x]) {}\mRightarrow{} \mforall{}\msubb{}x(:T) \mmember{} as. P[x] = \mforall{}\msubb{}x(:T) \mmember{} bs. Q[x])
Date html generated:
2019_10_16-PM-01_03_17
Last ObjectModification:
2018_10_08-AM-11_25_53
Theory : list_2
Home
Index