Step
*
1
of Lemma
fun-path-fixedpoint
1. T : Type
2. f : T ⟶ T
⊢ ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ []) and z=f*(x) via [])
BY
{ (RepUR ``fun-path`` 0 THEN Auto)⋅ }
Latex:
Latex:
1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
\mvdash{}  \mforall{}[x,y,z:T].    (y  =  z)  supposing  (((f  y)  =  y)  and  (y  \mmember{}  [])  and  z=f*(x)  via  [])
By
Latex:
(RepUR  ``fun-path``  0  THEN  Auto)\mcdot{}
Home
Index