%
\begin{isabellebody}%
\setisabellecontext{Isomorphisms}%
%
\isamarkupsection{Isomorphisms of set families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Isomorphisms\isanewline
\isakeyword{imports}\ Main\isanewline
\ \ {\isachardoublequoteopen}More{\isacharslash}MoreSet{\isachardoublequoteclose}\ {\isachardoublequoteopen}More{\isacharslash}MoreFun{\isachardoublequoteclose}\isanewline
\ \ UnionClosed\ Frankl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
Each injective function \isa{f} on the domain \isa{{\isasymUnion}\ F}
maps the set family \isa{F} to its isomorphic image \isa{op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F}. Elements of \isa{{\isasymUnion}\ F} are mapped using \isa{f}, while
elements of \isa{F} are mapped using \isa{op\ {\isacharbackquote}\ f}.%
\end{isamarkuptext}\isamarkuptrue%
%
\isamarkupsubsection{Properites preserved by injective functions%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ empty{\isacharunderscore}iso{\isacharcolon}\ {\isachardoublequoteopen}F\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}op\ {\isacharbackquote}\ f{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharunderscore}strong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}op\ {\isacharbackquote}\ f{\isacharparenright}\ {\isacharparenleft}Pow\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ F\ {\isasymlongleftrightarrow}\ finite\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharbrackleft}of\ f\ F{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharcolon}\ finite{\isacharunderscore}imageD{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ card\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ card{\isacharunderscore}image{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}f\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}elems{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}S{\isasymin}F{\isachardot}\ finite\ S{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymforall}S{\isasymin}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardot}\ finite\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ S\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ S\ {\isasymin}\ {\isacharquery}F{\isachardot}\ finite\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ finite{\isacharunderscore}imageD{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}f\ {\isacharbackquote}\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ S\ {\isasymin}\ {\isacharquery}F{\isachardot}\ finite\ S{\isacharbackquoteclose}\ {\isacharbackquoteopen}S\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}S\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}S\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assms{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}elem{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ A\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}f\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharequal}\ card\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iff{\isacharunderscore}eq{\isacharunderscore}card{\isacharbrackleft}of\ A\ f{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ f\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ A{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}ge{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}finite{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}Union{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharequal}\ finite\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenleft}subst\ finiteUn{\isacharunderscore}iff{\isacharparenright}{\isacharplus}{\isacharcomma}\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}iso\ finite{\isacharunderscore}elems{\isacharunderscore}iso{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F\ {\isasymlongleftrightarrow}\ union{\isacharunderscore}closed\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\ x\ y\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ x\ {\isasymunion}\ f\ {\isacharbackquote}\ y\ {\isasymin}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}x\ {\isasymunion}\ y{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymunion}\ y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isasymunion}\ f\ {\isacharbackquote}\ B\ {\isasymin}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ X\ \isakeyword{where}\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ X\ {\isacharequal}\ f\ {\isacharbackquote}\ A\ {\isasymunion}\ f\ {\isacharbackquote}\ B{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ X\ {\isacharequal}\ f\ {\isacharbackquote}\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isacharequal}\ A\ {\isasymunion}\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}X\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharunderscore}strong{\isacharbrackleft}of\ f\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}X\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F\ {\isasymlongleftrightarrow}\ finite{\isacharunderscore}union{\isacharunderscore}closed\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}Union{\isacharunderscore}iso{\isacharbrackleft}of\ f\ F{\isacharbrackright}\ union{\isacharunderscore}closed{\isacharunderscore}iso{\isacharbrackleft}of\ f\ F{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ count{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}count\ a\ F\ {\isacharequal}\ count\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ card{\isacharunderscore}image{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}aF\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}fafF\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}S\ {\isasymin}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardot}\ f\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}f\ {\isacharquery}aF{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ \isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}iso{\isacharbrackleft}of\ f\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f{\isachardoublequoteclose}\ F\ {\isacharquery}aF{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}aF{\isacharparenright}\ {\isacharequal}\ card\ {\isacharquery}fafF{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}aF\ {\isacharequal}\ {\isacharquery}fafF{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ a{\isacharprime}\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}a{\isacharprime}\ {\isasymin}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ a\ {\isacharequal}\ f\ a{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isasymin}\ {\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}aF{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ A\ {\isacharquery}aF\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}A\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}a{\isacharprime}\ {\isasymin}\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Frankl{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl\ F\ {\isasymlongleftrightarrow}\ frankl\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ X\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}X\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymand}\ card\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f\ x{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ count{\isacharunderscore}iso{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}iso{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ X\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}card\ {\isacharquery}F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharquery}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isasymUnion}F\ {\isasymand}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}x{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ \ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ count{\isacharunderscore}iso{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}iso{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharparenright}\ {\isacharequal}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ {\isacharparenleft}closure\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isacharequal}\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharasterisk}\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ subset{\isacharunderscore}image{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}g\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isacharequal}\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}{\isacharprime}\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}g\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ {\isasymUnion}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharprime}\ {\isasymsubseteq}\ {\isacharparenleft}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}g\ {\isacharbackquote}\ x\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}g\ {\isacharbackquote}\ x\ {\isasymin}\ closure\ {\isacharparenleft}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}F{\isachardot}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc\ {\isasymsubseteq}\ F\ {\isasymand}\ finite{\isacharunderscore}union{\isacharunderscore}closed\ F\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ a\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc{\isacharparenright}{\isacharparenright}{\isachardot}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}Fc\ {\isasymsubseteq}\ {\isasymUnion}F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}Fc\ {\isasymunion}\ {\isasymUnion}F\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}inj{\isacharunderscore}extend{\isacharbrackleft}of\ f\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isacharminus}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f{\isacharprime}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc\ {\isasymsubseteq}\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ x\ {\isasymin}\ op\ {\isacharbackquote}\ f{\isacharprime}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ x\ {\isacharequal}\ f{\isacharprime}\ {\isacharbackquote}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}iso\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ a\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ Fc{\isacharparenright}{\isacharparenright}{\isachardot}\ card\ {\isacharquery}F{\isacharprime}\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ {\isacharquery}F{\isacharprime}\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymUnion}\ Fc\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ a\ {\isacharequal}\ f{\isacharprime}\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}a{\isasymin}{\isasymUnion}Fc{\isachardot}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ count{\isacharunderscore}iso{\isacharbrackleft}of\ f{\isacharprime}\ F\ a{\isacharbrackright}\ card{\isacharunderscore}iso{\isacharbrackleft}of\ f{\isacharprime}\ F{\isacharbrackright}\ \ {\isacharbackquoteopen}inj{\isacharunderscore}on\ f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}a{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Injective embedding%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ inj{\isacharunderscore}embed\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ f{\isachardot}\ inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\ F{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}op\ {\isacharbackquote}\ f{\isacharparenright}\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}refl\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}id{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}sym{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F{\isacharprime}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ f\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}op\ {\isacharbackquote}\ f{\isacharparenright}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}f{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}inv{\isacharunderscore}into\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ f{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}f{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}f{\isacharprime}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ inj{\isacharunderscore}on{\isacharunderscore}inv{\isacharunderscore}into{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isacharequal}\ op\ {\isacharbackquote}\ {\isacharquery}f{\isacharprime}\ {\isacharbackquote}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isacharbackquote}\ {\isacharquery}f{\isacharprime}\ {\isacharbackquote}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ x{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharbackquoteopen}x\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ inv{\isacharunderscore}into\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ f\ {\isacharbackquote}\ f\ {\isacharbackquote}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inv{\isacharunderscore}into{\isacharunderscore}image{\isacharunderscore}cancel{\isacharbrackleft}of\ f\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}x\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ f\ {\isacharbackquote}\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}f{\isacharprime}\ {\isacharbackquote}\ x\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inv{\isacharunderscore}into{\isacharunderscore}image{\isacharunderscore}cancel{\isacharbrackleft}of\ f\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\ y{\isacharbrackright}\ {\isacharasterisk}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}trans{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ f\ g\ \isakeyword{where}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ g\ {\isacharparenleft}{\isasymUnion}F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}g\ {\isasymcirc}\ f{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ comp{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Isomoprhism definition%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
There is a bijective mapping between equivalent families.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ iso\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ h{\isachardot}\ bij{\isacharunderscore}betw\ h\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharprime}{\isacharparenright}\ {\isasymand}\ F{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}op\ {\isacharbackquote}\ h{\isacharparenright}\ {\isacharbackquote}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}\ {\isasymlongleftrightarrow}\ iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}F{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}op\ {\isacharbackquote}\ f{\isacharparenright}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\ inj{\isacharunderscore}embed{\isacharunderscore}def\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}refl{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso\ F\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}refl\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}sym{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharbrackright}\ \ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F{\isacharprime}\ F{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}sym\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}trans{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharbrackright}\ \ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ F\ F{\isacharprime}{\isacharprime}{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}trans{\isacharbrackleft}of\ F\ F{\isacharprime}\ F{\isacharprime}{\isacharprime}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}finite{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ F\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ F\ {\isasymlongleftrightarrow}\ finite\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ bij{\isacharunderscore}betw{\isacharunderscore}imp{\isacharunderscore}inj{\isacharunderscore}on\ finite{\isacharunderscore}iso{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}insert{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}{\isasymUnion}F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}card\ {\isacharparenleft}f\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharequal}\ card\ A{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isasymsubseteq}\ f\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}A\ {\isasymnotin}\ F\ {\isasymLongrightarrow}\ f\ {\isacharbackquote}\ A\ {\isasymnotin}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ \ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule\ conjI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}{\isacharparenleft}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Un{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F\ {\isasymunion}\ {\isacharbraceleft}f\ {\isacharbackquote}\ A{\isacharbraceright}\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}f\ {\isacharbackquote}\ A{\isacharparenright}\ {\isacharequal}\ card\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}image{\isacharbrackleft}of\ f\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isasymsubseteq}\ f\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}F\ {\isasymunion}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnotin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isasymnotin}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ F{\isachardoublequoteclose}\ \isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}f\ {\isacharbackquote}\ A\ {\isacharequal}\ f\ {\isacharbackquote}\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ f\ {\isacharparenleft}A\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}Un{\isacharunderscore}image{\isacharunderscore}eq{\isacharunderscore}iff{\isacharbrackleft}of\ f\ A\ A{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymnotin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Iso-representing collections of families%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FF' iso-represents FF if an isomporphic image of each element of FF is in FF'%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ iso{\isacharunderscore}represents\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ FF{\isacharprime}\ FF\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymforall}\ F\ {\isasymin}\ FF{\isachardot}\ {\isasymexists}\ F{\isacharprime}\ {\isasymin}\ FF{\isacharprime}{\isachardot}\ iso\ F\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ iso{\isacharunderscore}representing{\isacharunderscore}subset\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ FF{\isacharprime}\ FF\ {\isasymequiv}\ iso{\isacharunderscore}represents\ FF{\isacharprime}\ FF\ {\isasymand}\ FF{\isacharprime}\ {\isasymsubseteq}\ FF{\isachardoublequoteclose}\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
