---

Step * of Lemma all_rng_quot_elim_a

∀r:CRng. ∀p:Ideal(r){i}.
  ((∀x:|r|. SqStable(p x))
  ⇒ (∀d:detach_fun(|r|;p)
        ∀[F:|r / d| ⟶ ℙ]. ((∀w:|r / d|. SqStable(F[w])) ⇒ (∀w:|r / d|. F[w] ⇐⇒ ∀w:|r|. F[[w]{|r / d|}]))))
BY
{ (Unfold `type_inj` 0   THEN InstLemma `all_rng_quot_elim` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}p:Ideal(r)\{i\}.
    ((\mforall{}x:|r|.  SqStable(p  x))
    {}\mRightarrow{}  (\mforall{}d:detach\_fun(|r|;p)
                \mforall{}[F:|r  /  d|  {}\mrightarrow{}  \mBbbP{}]
                    ((\mforall{}w:|r  /  d|.  SqStable(F[w]))  {}\mRightarrow{}  (\mforall{}w:|r  /  d|.  F[w]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}w:|r|.  F[[w]\{|r  /  d|\}]))))


By

---

Latex:
(Unfold  `type\_inj`  0      THEN  InstLemma  `all\_rng\_quot\_elim`  []  THEN  Trivial)

---

Home Index