Theory CZH_Sets_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

chapter‹Set Theory for Category Theory›

theory CZH_Sets_Introduction


This chapter presents a formalization of the elements of set theory in 
the object logic ZFC in HOL› (cite"paulson_zermelo_2019", also see
of the formal proof assistant Isabelle cite"paulson_natural_1986".
The emphasis of this work is on the improvement of the convenience of the 
formalization of abstract mathematics internalized in the type typV.

subsection‹References, related and previous work›

The results that are presented in this chapter cannot be traced to a single
source of information. Nonetheless, the results are not original. 
A significant number of these results was carried over (with amendments) 
from the main library of Isabelle/HOL cite"noauthor_isabellehol_2020". 
Other results were inspired by elements of the content of the books 
Introduction to Axiomatic Set Theory› by G. Takeuti 
and W. M. Zaring cite"takeuti_introduction_1971", Theory of Sets› 
by N. Bourbaki cite"bourbaki_elements_1970" and Algebra› by 
T. W. Hungerford cite"hungerford_algebra_2003".
Furthermore, several online encyclopedias and forums 
(including Wikipedia cite"noauthor_wikipedia_2001", 
ProofWiki cite"noauthor_proofwiki_nodate", 
Encyclopedia of Mathematics cite"noauthor_encyclopedia_nodate",
nLab cite"noauthor_nlab_nodate" and Mathematics Stack Exchange) 
were used consistently throughout the development of this chapter. 
Inspiration for the work presented in this chapter has also been drawn 
from a similar ongoing project
in the formalization of mathematics in the system 
HOTG (Higher Order Tarski-Grothendieck) 
cite"brown_higher-order_2019" and "chen_hotg_2021".

It should also be mentioned that the Isabelle/HOL and the Isabelle/ML code 
from the main distribution of Isabelle2020 and certain posts on the 
mailing list of Isabelle were frequently reused
(with amendments) during the development of this chapter. Some of the 
specific examples of such reuse are 
\item The adoption of the implementation of
the command @{command lemmas_with} that is available as part of 
the framework Types-To-Sets in the main distribution of Isabelle2020.
\item The notation for the ``multiway-if'' was written
by Manuel Eberl and appeared in a post on the mailing list of Isabelle:

hide_const (open) list.set Sum subset 

lemmas ord_of_nat_zero = ord_of_nat.simps(1)


abbreviation (input) qm ((_ ? _ : _) [0, 0, 10] 10) 
  where "C ? A : B  if C then A else B"
abbreviation (input) if2 where "if2 a b  (λi. (i = 0 ? a : b))"

subsection‹Further foundational results›

lemma theD:
  assumes "∃!x. P x" and "x = (THE x. P x)"
  shows "P x" and "P y  x = y"
  using assms by (metis theI)+

lemmas [intro] = bij_betw_imageI

lemma bij_betwE[elim]:
  assumes "bij_betw f A B" and " inj_on f A; f ` A = B   P"
  shows P
  using assms unfolding bij_betw_def by auto

lemma bij_betwD[dest]:
  assumes "bij_betw f A B"
  shows "inj_on f A" and "f ` A = B"
  using assms by auto

lemma ex1D: "∃!x. P x  P x  P y  x = y" by clarsimp