Proof of proveit.numbers.ordering.min_y_le_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, min_def_bin
In [2]:
%proving min_y_le_x
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
min_y_le_x:
(see dependencies)
min_y_le_x:
(see dependencies)
In [3]:
defaults.assumptions = min_y_le_x.conditions
defaults.assumptions: 
In [4]:
min_def_bin
In [5]:
min_x_y = min_def_bin.instantiate({x: x, y: y}, auto_simplify=False)
min_x_y: 
, 
⊢ 
, 
⊢ 
We proceed by breaking the assumption $y \ge x$ into 2 cases¶
In [6]:
less_eq_def
In [7]:
y_le_x_def = less_eq_def.instantiate({x: y, y: x})
y_le_x_def: ⊢ 
In [8]:
y_le_x_def.derive_right_via_equality()
Case 1: $y < x$¶
In [9]:
min_x_y_is_y_if_y_less_x = min_x_y.inner_expr().rhs.simplify(assumptions=[InSet(x, Real), InSet(y, Real), Less(y, x)])
min_x_y_is_y_if_y_less_x: , , 
⊢ 
, , 
⊢ 
Case 2: $y = x$¶
In [10]:
greater_eq(y, x).prove(assumptions=[InSet(x, Real), InSet(y, Real), Equals(y, x)])
, , 
⊢ 
In [11]:
min_x_y_when_y_eq_x = min_x_y.inner_expr().rhs.simplify(assumptions=[InSet(x, Real), InSet(y, Real), Equals(y, x)])
min_x_y_when_y_eq_x: , , 
⊢ 
, , ⊢ 
In [12]:
# Use the fact that x = y to substitute
min_x_y_when_y_eq_x.inner_expr().rhs.substitute(y, assumptions=[Equals(y, x)], auto_simplify=False)
, , ⊢
Combine the 2 cases¶
In [13]:
y_le_x_def.rhs.derive_via_singular_dilemma(
min_x_y_is_y_if_y_less_x.expr)
, , ⊢
In [14]:
%qed
Out[14]:
