Last January 24, I moved Fpow into Main and introduced
Library/Equipollence.thy. Hope you like it.
Larry
> On 26 Jan 2019, at 15:14, Andrei Popescu wrote:
>
> Sorry for my late reply. I agree it makes sense to move such basic operators
> (and facts) into Main. The Ordinals and Cardinals
lanchette
Cc: Traytel Dmitriy , isabelle-dev
Subject: Re: [isabelle-dev] [Spam] cardinality primitives in
Isabelle/HOL?
Message-ID:
Content-Type: text/plain; charset=utf-8
This makes perfect sense to me.
I suggest moving at least the definition of Fpow into Main (it?s small, a
The question of dependency is tricky. I tried deleting the reference to
HOL-Cardinals.Cardinals and found that most of the elementary results were
easily provable using other library facts. But then there was this:
lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
by (meson card_of_ordLeq
Hi Larry,
if you want to put the definitions and the basic properties in Main, then
Fun.thy would probably be the place. But then I would argue that the syntax
should be hidden, as users might want to use these symbols for something else.
For the advanced material, do you need some theorems
I’m trying to install some of my new material and I’m wondering what to do with
equipollence and related concepts:
definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
where "eqpoll A B ≡ ∃f. bij_betw f A B"
definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
where
> On 28 Dec 2018, at 19:36, Lawrence Paulson wrote:
>
> Tons of useful stuff here.
>
> Some syntactic ambiguities, particularly around the =o relation, which is
> also defined as Set_Algebras.elt_set_eq.
True. The same holds for +o and *o (which are less widely used in the ordinals
Tons of useful stuff here.
Some syntactic ambiguities, particularly around the =o relation, which is also
defined as Set_Algebras.elt_set_eq.
I don’t suppose there’s any chance of using quotients to define actual
cardinals and use ordinary equality? And it still makes sense to introduce the
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,
14 matches
Mail list logo
