I am inclined to introduce these definitions:
definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"
definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
where "eqpoll A B ≡ ∃f. bij_betw f A B”
They allow, for example, this:
theorem Schroeder_Bernstein_eqpoll:
assumes "A ≲ B" "B ≲ A" shows "A ≈ B"
using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
The names and syntax are borrowed from Isabelle/ZF, and they are needed for
some HOL Light proofs.
But do they exist in some form already? And are there any comments on those
relation symbols?
Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
