permutation.bijn_transpose
∀ n i j, i ≤ n ⇒ j ≤ n ⇒ bijn (transpose i j) n
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.
theorem bijn_transpose : \forall (n:nat). \forall (i:nat). \forall (j:nat). ((le) i n) -> ((le) j n) -> (bijn) ((transpose) i j) n.
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).
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))))))
Printing for OpenTheory is not working at the moment.