Step
*
of Lemma
sp-lub_wf
∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) ∈ Sierpinski)
BY
{ ((D 0 THENA Auto)
THEN (InstLemma `quotient-function-subtype` [⌜ℕ⌝;⌜ℕ ⟶ 𝔹⌝;⌜λ2f g.f = ⊥ ∈ (ℕ ⟶ 𝔹)
⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)⌝]⋅ THENA Auto)
THEN Fold `Sierpinski` (-1)
THEN BLemma `sp-lub_wf1`
THEN SubsumeC ⌜ℕ ⟶ Sierpinski⌝⋅
THEN Auto) }
Latex:
Latex:
\mforall{}[A:\mBbbN{} {}\mrightarrow{} Sierpinski]. (lub(n.A[n]) \mmember{} Sierpinski)
By
Latex:
((D 0 THENA Auto)
THEN (InstLemma `quotient-function-subtype` [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{} {}\mrightarrow{} \mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f g.f = \mbot{} \mLeftarrow{}{}\mRightarrow{} g = \mbot{}\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Fold `Sierpinski` (-1)
THEN BLemma `sp-lub\_wf1`
THEN SubsumeC \mkleeneopen{}\mBbbN{} {}\mrightarrow{} Sierpinski\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index