Menu Close

Si a, b, c ∈ ℝ, entonces min(min(a,b),c) = min(a,min(b,c))

Sean a, b y c números reales. Demostrar que

   min (min a b) c = min a (min b c)

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

import data.real.basic tactic
variables a b c : 
 
example :
  min (min a b) c = min a (min b c) :=
sorry

Soluciones con Lean

import data.real.basic tactic
 
variables a b c : 
 
-- 1ª demostración
-- ===============
 
-- Se usará el siguiente lema auxilar.
lemma aux1 : min (min a b) c  min a (min b c) :=
begin
  apply le_min,
  { show min (min a b) c  a,
      calc min (min a b) c
            min a b : min_le_left (min a b) c
       ...  a       : min_le_left a b },
  { show min (min a b) c  min b c,
    apply le_min,
    { show min (min a b) c  b,
        calc min (min a b) c
              min a b  : min_le_left (min a b) c
         ...  b        : min_le_right a b },
    { show min (min a b) c  c,
      { by exact min_le_right (min a b) c }}},
end
 
example :
  min (min a b) c = min a (min b c) :=
begin
  apply le_antisymm,
  { show min (min a b) c  min a (min b c),
      by exact aux1 a b c },
  { show min a (min b c)  min (min a b) c,
      calc min a (min b c)
           = min (min b c) a : by apply min_comm
       ... = min (min c b) a : by {congr' 1, apply min_comm}
       ...  min c (min b a) : by apply aux1
       ... = min c (min a b) : by {congr' 1, apply min_comm}
       ... = min (min a b) c : by apply min_comm },
end
 
-- 2ª demostración
-- ===============
 
-- Se usará el siguiente lema auxilar.
lemma aux2 : min (min a b) c  min a (min b c) :=
begin
  apply le_min,
  { calc min (min a b) c
          min a b : by simp [min_le_left]
     ...  a       : by simp [min_le_left] },
  { apply le_min,
    { calc min (min a b) c
            min a b  : by simp [min_le_left]
       ...  b        : by simp [min_le_right] },
    { simp [min_le_right] }},
end
 
example : min (min a b) c = min a (min b c) :=
begin
  apply le_antisymm,
  { by exact aux2 a b c },
  { calc min a (min b c)
         = min (min b c) a : by simp [min_comm]
     ... = min (min c b) a : by simp [min_comm]
     ...  min c (min b a) : by simp [aux2]
     ... = min c (min a b) : by simp [min_comm]
     ... = min (min a b) c : by simp [min_comm] },
end
 
-- 3ª demostración
-- ===============
 
example : min (min a b) c = min a (min b c) :=
begin
  apply le_antisymm,
  { by exact aux2 a b c },
  { calc min a (min b c)
         = min (min c b) a : by simp [min_comm]
     ...  min c (min b a) : by simp [aux2]
     ... = min (min a b) c : by simp [min_comm] },
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

Leave a Reply