equal
deleted
inserted
replaced
919 @{thm[mode=IfThen] finite_imageD} |
919 @{thm[mode=IfThen] finite_imageD} |
920 \end{equation} |
920 \end{equation} |
921 |
921 |
922 \noindent |
922 \noindent |
923 It states that if an image of a set under an injective function @{text f} (injective over this set) |
923 It states that if an image of a set under an injective function @{text f} (injective over this set) |
924 is finite, then @{text A} itself must be finite. We can use it to establish the following |
924 is finite, then the set @{text A} itself must be finite. We can use it to establish the following |
925 two lemmas. |
925 two lemmas. |
926 |
926 |
927 \begin{lemma}\label{finone} |
927 \begin{lemma}\label{finone} |
928 @{thm[mode=IfThen] finite_eq_tag_rel} |
928 @{thm[mode=IfThen] finite_eq_tag_rel} |
929 \end{lemma} |
929 \end{lemma} |
1155 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1155 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1156 \end{proof} |
1156 \end{proof} |
1157 |
1157 |
1158 \noindent |
1158 \noindent |
1159 The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When |
1159 The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When |
1160 we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"} and @{text x} is not the |
1160 we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the |
1161 empty string, we |
1161 empty string, we |
1162 have the following picture: |
1162 have the following picture: |
1163 |
1163 |
1164 \begin{center} |
1164 \begin{center} |
1165 \scalebox{0.7}{ |
1165 \scalebox{0.7}{ |