On 27/12/2018 17:45, Traytel Dmitriy wrote:
> 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
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
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"
> On 27 Dec 2018, at 12:45, Florian Haftmann
> wrote:
>
> (I don't know how useful the strict versions less_poll, greater_poll
> would be).
Strict versions do turn up in some places (both in HOL Light and Isabelle/ZF)
___
isabelle-dev mailing list
>> Anyway, I am uncertain about the name »poll«.
>
> From https://en.wikipedia.org/wiki/Cardinality
>
> "Two sets A and B have the same cardinality if there exists a bijection from
> A to B, that is, a function from A to B that is both injective and
> surjective. Such sets are said to be
> On 27 Dec 2018, at 12:39, Florian Haftmann
> wrote:
Thanks for the suggestions.
> The input abbreviation gepoll should be added as well.
>
> Anyway, I am uncertain about the name »poll«.
From https://en.wikipedia.org/wiki/Cardinality
"Two sets A and B have the same cardinality if there
> 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,
