---

Step * 1 of Lemma sub-corec-family


1. P : Type
2. H : (P ⟶ Type) ⟶ P ⟶ Type
3. ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
4. ⋂n:ℕ. H (H^n (λp.Top)) ⊆ H ⋂n:ℕ. H^n (λp.Top)
⊢ ⋂n:ℕ. H^n (λp.Top) ⊆ ⋂n:ℕ. H (H^n (λp.Top))
BY
{ TACTIC:(RepUR ``isect-family`` 0 THEN D 0 THEN Reduce 0 THEN Auto THEN BLemma `subtype_rel_isect` THEN Auto) }

1
1. P : Type
2. H : (P ⟶ Type) ⟶ P ⟶ Type
3. ∀[X:ℕ ⟶ P ⟶ Type]. ⋂n:ℕ. H (X n) ⊆ H ⋂n:ℕ. X n
4. ⋂n:ℕ. H (H^n (λp.Top)) ⊆ H ⋂n:ℕ. H^n (λp.Top)
5. p : P@i
6. n : ℕ
⊢ (⋂n:ℕ. (H^n (λp.Top) p)) ⊆r (H (H^n (λp.Top)) p)

---

Latex:

---

Latex:

1.  P  :  Type
2.  H  :  (P  {}\mrightarrow{}  Type)  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
3.  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].  \mcap{}n:\mBbbN{}.  H  (X  n)  \msubseteq{}  H  \mcap{}n:\mBbbN{}.  X  n
4.  \mcap{}n:\mBbbN{}.  H  (H\^{}n  (\mlambda{}p.Top))  \msubseteq{}  H  \mcap{}n:\mBbbN{}.  H\^{}n  (\mlambda{}p.Top)
\mvdash{}  \mcap{}n:\mBbbN{}.  H\^{}n  (\mlambda{}p.Top)  \msubseteq{}  \mcap{}n:\mBbbN{}.  H  (H\^{}n  (\mlambda{}p.Top))


By

---

Latex:
TACTIC:(RepUR  ``isect-family``  0
                THEN  D  0
                THEN  Reduce  0
                THEN  Auto
                THEN  BLemma  `subtype\_rel\_isect`
                THEN  Auto)

---

Home Index