# Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

```Hi Larry,

the HOL-Cardinals library might be just right for the purpose:```
```
theory Scratch
imports "HOL-Cardinals.Cardinals"
begin

lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
by (rule card_of_ordLeq[symmetric])

lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
by (rule card_of_ordIso[symmetric])

lemma
assumes "|A| ≤o |B|" "|B| ≤o |A|"
shows "|A| =o |B|"
by (simp only: assms ordIso_iff_ordLeq)

end

The canonical entry point for the library is the above HOL-Cardinals.Cardinals.
Many of the theorems and definitions are already in Main, because the
(co)datatype package is based on them. The syntax is hidden in main—one gets it
by importing HOL-Library.Cardinal_Notations (which HOL-Cardinals.Cardinals does
transitively).

Our ITP'14 paper explains the design of the library:

http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf

Dmitriy

> On 27 Dec 2018, at 13:31, Lawrence Paulson <l...@cam.ac.uk> wrote:
>
> 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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
```