Email Gateway (Aug 22 2022 at 13:39): Email Gateway (Aug 22 2022 at 13:39):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Deal all
I'm looking for the essential definition of ordered pair in Isabelle/HOL as
I found it in Isabelle/ZF but I need it on HOL and I found some theories in
Isabelle/HOL like : Product_Type,Relation, Fun_Def, Function_Order,
Relators, BNF_Def, Wellfounded and many other theories. My question is
where I can find the essential definition of ordered pair product as a
function. I've seen the product definition in Product_Type theory but I
still can't find the definition of ordered pair as in set theory (as a
function).
So, is there and function or definition says that the ('a x'b)set is a
function or relation of AXB where for pair (a,b):C a:A and b:B and C is
('a x'b)set.
Cheers
Jasim
Last updated: Apr 19 2024 at 08:19 UTC