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

```I agree with Florian wrt syntax.

Tobias```
```
On 27/12/2018 13:39, Florian Haftmann 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?
```
```
The notation itself is quite generic, so it is worth spending more
thoughts on how can we keep reusable.  Maybe it would be worth a try to
put the syntax into a bundle (there are already some applications of
that pattern):

bundle set_relation_syntax
begin

notation …

end

bundle no_set_relation_syntax
begin

no_notation …

end

…

unbundle set_relation_syntax

…

unbundle no_set_relation_syntax

The input abbreviation gepoll should be added as well.

Anyway, I am uncertain about the name »poll«.

Cheers,
Florian

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

```
```
```

smime.p7s
Description: S/MIME Cryptographic Signature

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