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

[Lawrence Paulson]

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