Menu Close

Si a, b ∈ ℝ, entonces max(a,b) = max(b,a)

Demostrar que si a, b ∈ ℝ, entonces max(a,b) = max(b,a)

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

import data.real.basic
 
variables a b : 
 
example : max a b = max b a :=
sorry

Soluciones con Lean

import data.real.basic
 
variables a b : 
 
-- 1ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  apply le_antisymm,
  { show max a b  max b a,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
  { show max b a  max a b,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
end
 
-- 2ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  have h :  x y : , max x y  max y x,
  { intros x y,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
  apply le_antisymm,
  apply h,
  apply h,
end
 
-- 3ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  have h :  {x y : }, max x y  max y x,
  { intros x y,
    exact max_le (le_max_right y x) (le_max_left y x),},
  exact le_antisymm h h,
end
 
-- 4ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  apply le_antisymm,
  repeat {
    apply max_le,
    apply le_max_right,
    apply le_max_left },
end

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

Referencias

Leave a Reply