<commit_before>(*  Title:      ZF/Cardinal.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Cardinals in Zermelo-Fraenkel Set Theory 
*)

Cardinal = OrderType + Fixedpt + Nat + Sum + 
consts
  Least            :: (i=>o) => i    (binder "LEAST " 10)
  eqpoll, lepoll,
          lesspoll :: [i,i] => o     (infixl 50)
  cardinal         :: i=>i           ("|_|")
  Finite, Card     :: i=>o

defs

  (*least ordinal operator*)
  Least_def     "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"

  eqpoll_def    "A eqpoll B == EX f. f: bij(A,B)"

  lepoll_def    "A lepoll B == EX f. f: inj(A,B)"

  lesspoll_def  "A lesspoll B == A lepoll B & ~(A eqpoll B)"

  Finite_def    "Finite(A) == EX n:nat. A eqpoll n"

  cardinal_def  "|A| == LEAST i. i eqpoll A"

  Card_def      "Card(i) == (i = |i|)"

syntax (xsymbols)
  "op eqpoll"      :: [i,i] => o     (infixl "\\<approx>" 50)
  "op lepoll"      :: [i,i] => o     (infixl "\\<lesssim>" 50)
  "op lesspoll"    :: [i,i] => o     (infixl "\\<prec>" 50)

end
<commit_msg>mu-syntax for the LEAST operator<commit_after>(*  Title:      ZF/Cardinal.thy
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Cardinals in Zermelo-Fraenkel Set Theory 
*)

Cardinal = OrderType + Fixedpt + Nat + Sum + 
consts
  Least            :: (i=>o) => i    (binder "LEAST " 10)
  eqpoll, lepoll,
          lesspoll :: [i,i] => o     (infixl 50)
  cardinal         :: i=>i           ("|_|")
  Finite, Card     :: i=>o

defs

  (*least ordinal operator*)
  Least_def     "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"

  eqpoll_def    "A eqpoll B == EX f. f: bij(A,B)"

  lepoll_def    "A lepoll B == EX f. f: inj(A,B)"

  lesspoll_def  "A lesspoll B == A lepoll B & ~(A eqpoll B)"

  Finite_def    "Finite(A) == EX n:nat. A eqpoll n"

  cardinal_def  "|A| == LEAST i. i eqpoll A"

  Card_def      "Card(i) == (i = |i|)"

syntax (xsymbols)
  "op eqpoll"      :: [i,i] => o     (infixl "\\<approx>" 50)
  "op lepoll"      :: [i,i] => o     (infixl "\\<lesssim>" 50)
  "op lesspoll"    :: [i,i] => o     (infixl "\\<prec>" 50)
  "LEAST "         :: [pttrn, o] => i        ("(3\\<mu>_./ _)" [0, 10] 10)

end

{'fraction_non_alphanumeric': 0.17730802415875754, 'fraction_numerical': 0.014667817083692839, 'mean_word_length': 2.1551020408163266, 'pattern_counts': {'":': 0, '<': 14, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5789525', 'n_tokens_mistral': 995, 'n_tokens_neox': 925, 'n_words': 266}