Nuprl Lemma : mk_perm_wf_a
∀T:Type. ∀f,b:T ⟶ T. (InvFuns(T;T;f;b) ⇒ (mk_perm(f;b) ∈ Perm(T)))
Proof
Definitions occuring in Statement :
mk_perm: mk_perm(f;b),
perm: Perm(T),
inv_funs: InvFuns(A;B;f;g),
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
perm_f: p.f,
pi1: fst(t),
mk_perm: mk_perm(f;b),
perm_b: p.b,
pi2: snd(t),
perm: Perm(T),
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
mk_perm_wf,
inv_funs_wf,
perm_f_wf,
perm_b_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
sqequalHypSubstitution,
hypothesis,
dependent_set_memberEquality_alt,
introduction,
extract_by_obid,
dependent_functionElimination,
thin,
hypothesisEquality,
universeIsType,
isectElimination,
inhabitedIsType,
functionIsType,
universeEquality
Latex:
\mforall{}T:Type. \mforall{}f,b:T {}\mrightarrow{} T. (InvFuns(T;T;f;b) {}\mRightarrow{} (mk\_perm(f;b) \mmember{} Perm(T)))
Date html generated:
2019_10_16-PM-00_58_42
Last ObjectModification:
2018_10_08-AM-09_48_59
Theory : perms_1
Home
Index