// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

permutation.bijn_transpose

Statement

∀ n i j, i ≤ n ⇒ j ≤ n ⇒ bijn (transpose i j) n

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem bijn_transpose : forall (n:nat.nat), forall (i:nat.nat), forall (j:nat.nat), (nat.le i n) -> (nat.le j n) -> bijn (transpose i j) n.



Matita-Jumb
Statement

theorem bijn_transpose : \forall (n:nat). \forall (i:nat). \forall (j:nat). ((le) i n) -> ((le) j n) -> (bijn) ((transpose) i j) n.



Lean-jumb
Statement

theorem bijn_transpose : forall (n:nat.nat) , forall (i:nat.nat) , forall (j:nat.nat) , ((((nat.le_) ) (i)) (n)) -> ((((nat.le_) ) (j)) (n)) -> (((permutation.bijn) ) ((((permutation.transpose) ) (i)) (j))) (n).



PVS-jumb

Statement

bijn_transpose : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(i:nat_sttfa_th.sttfa_nat):(FORALL(j:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i)(n) => (nat_sttfa_th.le(j)(n) => permutation_sttfa.bijn(permutation_sttfa.transpose(i)(j))(n))))))



OpenTheory

Printing for OpenTheory is not working at the moment.