Demonstrations for the theory of proveit.core_expr_types.operations

import proveit
from proveit import Lambda, Conditional
from proveit import x, fx, gx, Qx, n
from proveit.logic import Equals, Forall
from proveit.numbers import Sum, Interval, one
%begin demonstrations

Instance substitution

domain = Interval(one, n)

domain:

universal_eq = Forall(x, Equals(fx, gx), domain=domain)

universal_eq:

summation = Sum(x, fx, domain=domain)

summation:

summation.instance_substitution(universal_eq, assumptions=[universal_eq])

 ⊢  

%end demonstrations