Step
*
of Lemma
satisfies-negate-poly-constraints
∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
  ((∀X∈L.¬satisfies-poly-constraints(f;X)) 
⇐⇒ (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X)))
BY
{ Assert ⌜∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
            ((∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X))
            
⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z))))⌝⋅ }
1
.....assertion..... 
∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
  ((∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X))
  
⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z))))
2
1. ∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
     ((∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X))
     
⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z))))
⊢ ∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
    ((∀X∈L.¬satisfies-poly-constraints(f;X)) 
⇐⇒ (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X)))
Latex:
Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:polynomial-constraints()  List.
    ((\mforall{}X\mmember{}L.\mneg{}satisfies-poly-constraints(f;X))
    \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}negate-poly-constraints(L).  satisfies-poly-constraints(f;X)))
By
Latex:
Assert  \mkleeneopen{}\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:polynomial-constraints()  List.
                    ((\mexists{}X\mmember{}negate-poly-constraints(L).  satisfies-poly-constraints(f;X))
                    \mLeftarrow{}{}\mRightarrow{}  (\mforall{}X\mmember{}L.(\mexists{}Z\mmember{}negate-poly-constraint(X).  satisfies-poly-constraints(f;Z))))\mkleeneclose{}\mcdot{}
Home
Index