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
> 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
library)
> Cardinals development.
>
> Where do people think these definitions and proofs should be installed?
>
> Larry
>
>> On 27 Dec 2018, at 20:29, Makarius wrote:
>>
>> On 27/12/2018 17:45, Traytel Dmitriy wrote:
>>> Hi Larry,
>>>
>>&g
