Step
*
of Lemma
es-fix-causle
∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:E(X) ─→ E(X). ((∀x:E(X). f x c≤ x)
⇒ (∀e:E(X). f**(e) c≤ e))
BY
{ ((UnivCD THENA Auto) THEN InstLemma `es-fix_property` [⌈Info⌉;⌈es⌉;⌈X⌉;⌈f⌉;⌈e⌉]⋅ THEN Auto) }
1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E(X)@i
5. ∀x:E(X). f x c≤ x@i
6. e : E(X)@i
7. (f f**(e)) = f**(e) ∈ E(X)
8. f**(e) is f*(e)
⊢ f**(e) c≤ e
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:E(X) {}\mrightarrow{} E(X). ((\mforall{}x:E(X). f x c\mleq{} x) {}\mRightarrow{} (\mforall{}e:E(X). f**(e) c\mleq{} e))
By
((UnivCD THENA Auto) THEN InstLemma `es-fix\_property` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index