---

Step * of Lemma corec-family-ext

∀[P:Type]. ∀[H:(P ⟶ Type) ⟶ P ⟶ Type].
  corec-family(H) ≡ H corec-family(H) supposing type-family-continuous{i:l}(P;H) ∧ family-monotone{i:l}(P;H)
BY
{ (Auto THEN BLemma `ext-family-iff` THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[H:(P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].
    corec-family(H)  \mequiv{}  H  corec-family(H) 
    supposing  type-family-continuous\{i:l\}(P;H)  \mwedge{}  family-monotone\{i:l\}(P;H)


By

---

Latex:
(Auto  THEN  BLemma  `ext-family-iff`  THEN  EAuto  1)

---

Home Index