Step * of Lemma stable__function_equal

[A,B:Type]. ∀[f,g:A ⟶ B].  Stable{f g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) (g x) ∈ B}
BY
(Unfold `stable` THEN Auto THEN FunExt THEN Auto) }


Latex:


Latex:
\mforall{}[A,B:Type].  \mforall{}[f,g:A  {}\mrightarrow{}  B].    Stable\{f  =  g\}  supposing  \mforall{}x:A.  Stable\{(f  x)  =  (g  x)\}


By


Latex:
(Unfold  `stable`  0  THEN  Auto  THEN  FunExt  THEN  Auto)




Home Index