### Nuprl Lemma : comb_for_txpose_perm_wf

`λn,i,j,z. txpose_perm(i;j) ∈ n:ℕ ⟶ i:ℕn ⟶ j:ℕn ⟶ (↓True) ⟶ Sym(n)`

Proof

Definitions occuring in Statement :  txpose_perm: txpose_perm sym_grp: `Sym(n)` int_seg: `{i..j-}` nat: `ℕ` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` nat: `ℕ`
Lemmas referenced :  txpose_perm_wf squash_wf true_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality_alt sqequalHypSubstitution imageElimination cut introduction extract_by_obid dependent_functionElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeIsType isectElimination inhabitedIsType natural_numberEquality setElimination rename

Latex:
\mlambda{}n,i,j,z.  txpose\_perm(i;j)  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  i:\mBbbN{}n  {}\mrightarrow{}  j:\mBbbN{}n  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  Sym(n)

Date html generated: 2019_10_16-PM-00_59_21
Last ObjectModification: 2018_10_08-AM-09_26_38

Theory : perms_1

Home Index