Step
*
of Lemma
uanti_sym_functionality_wrt_iff
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
uiff(UniformlyAntiSym(T;x,y.R[x;y]);UniformlyAntiSym(T;x,y.R'[x;y])) supposing ∀[x,y:T]. (R[x;y]
⇐⇒ R'[x;y])
BY
{ (((Unfold `uanti_sym` 0 THENM RepD) THENM RWW "-1" 0) THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[R,R':T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
uiff(UniformlyAntiSym(T;x,y.R[x;y]);UniformlyAntiSym(T;x,y.R'[x;y]))
supposing \mforall{}[x,y:T]. (R[x;y] \mLeftarrow{}{}\mRightarrow{} R'[x;y])
By
Latex:
(((Unfold `uanti\_sym` 0 THENM RepD) THENM RWW "-1" 0) THEN Auto)
Home
Index