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

Definition

permutation.bijn

Body

λf. λn. ∀ m, m ≤ n ⇒ ex (λp. (p ≤ n) ∧ ((f p) = m))

Main Dependencies
Theory

Coq-Jumb
Body

Definition bijn : (nat.nat -> nat.nat) -> nat.nat -> Prop := fun (f:(nat.nat -> nat.nat)) => fun (n:nat.nat) => forall (m:nat.nat), (nat.le m n) -> connectives.ex (nat.nat) (fun (p:nat.nat) => connectives.And (nat.le p n) (logic.eq (nat.nat) (f p) m))



Matita-Jumb
Body

definition bijn : (nat -> nat) -> nat -> Prop := \lambda f : nat -> nat. \lambda n : nat. \forall (m:nat). ((le) m n) -> (ex) (nat) (\lambda p : nat. (And) ((le) p n) ((eq) (nat) (f p) m))



Lean-jumb
Body

def bijn : ((nat.nat) -> nat.nat) -> (nat.nat) -> Prop := fun (f : (nat.nat) -> nat.nat) , fun (n : nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (m)) (n)) -> ((connectives.ex) (nat.nat)) (fun (p : nat.nat) , (((connectives.And) ) ((((nat.le_) ) (p)) (n))) ((((logic.eq_) (nat.nat)) ((f) (p))) (m)))



PVS-jumb

Body

bijn : [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [nat_sttfa_th.sttfa_nat -> bool]] = (LAMBDA(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(m)(n) => connectives_sttfa_th.sttfa_ex[nat_sttfa_th.sttfa_nat]((LAMBDA(p:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_And(nat_sttfa_th.le(p)(n))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(p))(m))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.