Proof of proveit.numbers.ordering.max_y_ge_x theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import x, y, defaults
from proveit.logic import Equals, InSet
from proveit.numbers import greater_eq, Less, Real
from proveit.numbers.ordering import less_eq_def, max_def_bin
In [2]:
%proving max_y_ge_x
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
max_y_ge_x:
(see dependencies)
max_y_ge_x:
(see dependencies)
In [3]:
defaults.assumptions = max_y_ge_x.conditions
defaults.assumptions: 
In [4]:
max_def_bin
In [5]:
max_x_y = max_def_bin.instantiate({x: x, y: y}, auto_simplify=False)
max_x_y: 
, 
⊢ 
, 
⊢ 
We proceed by breaking the assumption $y \ge x$ into 2 cases¶
In [6]:
less_eq_def
In [7]:
y_ge_x_def = less_eq_def.instantiate({x: x, y: y})
y_ge_x_def: ⊢ 
In [8]:
y_ge_x_def.derive_right_via_equality()
Case 1: $x < y$¶
In [9]:
max_x_y_is_y_if_x_less_y = max_x_y.inner_expr().rhs.simplify(assumptions=[InSet(x, Real), InSet(y, Real), Less(x, y)])
max_x_y_is_y_if_x_less_y: , , 
⊢ 
, , 
⊢ 
Case 2: $x = y$¶
In [10]:
greater_eq(x, y).prove(assumptions=[InSet(x, Real), InSet(y, Real), Equals(x, y)])
, , 
⊢ 
In [11]:
max_x_y_when_x_eq_y = max_x_y.inner_expr().rhs.simplify(assumptions=[InSet(x, Real), InSet(y, Real), Equals(x, y)])
max_x_y_when_x_eq_y: , , 
⊢ 
, , ⊢ 
In [12]:
# Use the fact that x = y to substitute
max_x_y_when_x_eq_y.inner_expr().rhs.substitute(y, assumptions=[Equals(x, y)], auto_simplify=False)
, , ⊢
Combine the 2 cases¶
In [13]:
or_version_of_thm = y_ge_x_def.rhs.derive_via_singular_dilemma(
max_x_y_is_y_if_x_less_y.expr)
or_version_of_thm: 
, , ⊢
, , ⊢ In [14]:
%qed
Out[14]:
