Minimo_de_suma.md

Título	Autor
En ℝ, min(a,b)+c = min(a+c,b+c)	José A. Alonso

Demostrar con Lean4 que si (a), (b) y (c) números reales, entonces [\min(a,b)+c = \min(a+c,b+c)]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

variable {a b c : ℝ}

example :
  min a b + c = min (a + c) (b + c) :=
by sorry

Demostraciones en lenguaje natural (LN)

[mathjax] 1ª demostración en LN

Aplicando la propiedad antisimétrica a las siguientes desigualdades \begin{align} \min(a, b) + c \leq \min(a + c, b + c) \tag{1} \ \min(a + c, b + c) \leq \min(a, b) + c \tag{2} \end{align}

Para demostrar (1) basta demostrar que se verifican las siguientes desigualdades \begin{align} \min(a, b) + c &\leq a + c \tag{1a} \ \min(a, b) + c &\leq b + c \tag{1b} \end{align} que se tienen porque se verifican las siguientes desigualdades \begin{align} \min(a, b) &\leq a \ \min(a, b) &\leq b \end{align}

Para demostrar (2) basta demostrar que se verifica [ \min(a + c, b + c) - c \leq \min(a, b) ] que se demuestra usando (1); en efecto, \begin{align} \min(a + c, b + c) - c &\leq \min(a + c - c, b + c - c) &&\text{[por (1)]}\ &= \min(a, b) \end{align}

2ª demostración en LN

Por casos según (a \leq b).

1º caso: Supongamos que (a \leq b). Entonces, \begin{align} \min(a, b) + c &= a + c \ &= \min(a + c, b + c) \end{align}

2º caso: Supongamos que (a \nleq b). Entonces, \begin{align} \min(a, b) + c &= b + c \ &= \min(a + c, b + c) \end{align}

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable {a b c : ℝ}

-- En las demostraciones se usarán los siguientes lemas auxiliares
--    aux1 : min a b + c ≤ min (a + c) (b + c)
--    aux2 : min (a + c) (b + c) ≤ min a b + c
-- cuyas demostraciones se exponen a continuación.

-- 1ª demostración de aux1
lemma aux1 :
  min a b + c ≤ min (a + c) (b + c) :=
by
  have h1 : min a b ≤ a :=
    min_le_left a b
  have h2 : min a b + c ≤ a + c :=
    add_le_add_right h1 c
  have h3 : min a b  ≤ b :=
    min_le_right a b
  have h4 : min a b + c ≤ b + c :=
    add_le_add_right h3 c
  show min a b + c ≤ min (a + c) (b + c)
  exact le_min h2 h4

-- 2ª demostración de aux1
example :
  min a b + c ≤ min (a + c) (b + c) :=
by
  apply le_min
  { apply add_le_add_right
    exact min_le_left a b }
  { apply add_le_add_right
    exact min_le_right a b }

-- 3ª demostración de aux1
example :
  min a b + c ≤ min (a + c) (b + c) :=
le_min (add_le_add_right (min_le_left a b) c)
       (add_le_add_right (min_le_right a b) c)

-- 1ª demostración de aux2
lemma aux2 :
  min (a + c) (b + c) ≤ min a b + c :=
by
  have h1 : min (a + c) (b + c) + -c ≤ min a b
  { calc min (a + c) (b + c) + -c
         ≤ min (a + c + -c) (b + c + -c) := aux1
       _ = min a b                       := by ring_nf }
  show min (a + c) (b + c) ≤ min a b + c
  exact add_neg_le_iff_le_add.mp h1

-- 1ª demostración del ejercicio
example :
  min a b + c = min (a + c) (b + c) :=
by
  have h1 : min a b + c ≤ min (a + c) (b + c) := aux1
  have h2 : min (a + c) (b + c) ≤ min a b + c := aux2
  show min a b + c = min (a + c) (b + c)
  exact le_antisymm h1 h2

-- 2ª demostración del ejercicio
example :
  min a b + c = min (a + c) (b + c) :=
by
  apply le_antisymm
  { show min a b + c ≤ min (a + c) (b + c)
    exact aux1 }
  { show min (a + c) (b + c) ≤ min a b + c
    exact aux2 }

-- 3ª demostración del ejercicio
example :
  min a b + c = min (a + c) (b + c) :=
by
  apply le_antisymm
  { exact aux1 }
  { exact aux2 }

-- 4ª demostración del ejercicio
example :
  min a b + c = min (a + c) (b + c) :=
le_antisymm aux1 aux2

-- 5ª demostración del ejercicio
example : min a b + c = min (a + c) (b + c) :=
by
  by_cases h : a ≤ b
  { have h1 : a + c ≤ b + c := add_le_add_right h c
    calc min a b + c = a + c               := by simp [min_eq_left h]
                   _ = min (a + c) (b + c) := by simp [min_eq_left h1]}
  { have h2: b ≤ a := le_of_not_le h
    have h3 : b + c ≤ a + c := add_le_add_right h2 c
    calc min a b + c = b + c               := by simp [min_eq_right h2]
                   _ = min (a + c) (b + c) := by simp [min_eq_right h3]}

-- 6ª demostración del ejercicio
example : min a b + c = min (a + c) (b + c) :=
(min_add_add_right a b c).symm

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 18.