418 Example of non-regularizable theorem ($0 = 1$).

   418   Example of non-regularizable theorem ($0 = 1$).

   419 

   419 

   420 Separtion of regularization from injection thanks to the following 2 lemmas:

   420 

   421 \begin{lemma}

   421   Separtion of regularization from injection thanks to the following 2 lemmas:

   422 If @{term R2} is an equivalence relation, then:

   422   \begin{lemma}

   423 \begin{eqnarray}

   423   If @{term R2} is an equivalence relation, then:

   424 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\

   424   \begin{eqnarray}

   425 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}

   425   @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\

   426 \end{eqnarray}

   426   @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}

   427 \end{lemma}

   427   \end{eqnarray}

   428   \end{lemma}

   429 

   430   Other lemmas used in regularization:

   431   @{thm [display] ball_reg_eqv[no_vars]}

   432   @{thm [display] bex_reg_eqv[no_vars]}

   433   @{thm [display] babs_reg_eqv[no_vars]}

   434   @{thm [display] babs_simp[no_vars]}

   435 

   436   @{thm [display] ball_reg_right[no_vars]}

   437   @{thm [display] bex_reg_left[no_vars]}

   438   @{thm [display] bex1_bexeq_reg[no_vars]}