Si a, b ∈ ℝ, entonces min(a,b) = min(b,a)
Demostrar que si a, b ∈ ℝ, entonces min(a,b) = min(b,a).
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 |
import data.real.basic variables a b : ℝ example : min a b = min b a := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 |
import data.real.basic variables a b : ℝ -- 1ª demostración -- =============== example : min a b = min b a := begin apply le_antisymm, { show min a b ≤ min b a, apply le_min, { apply min_le_right }, { apply min_le_left }}, { show min b a ≤ min a b, apply le_min, { apply min_le_right }, { apply min_le_left }}, end -- 2ª demostración -- =============== example : min a b = min b a := begin have h : ∀ x y : ℝ, min x y ≤ min y x, { intros x y, apply le_min, { apply min_le_right }, { apply min_le_left }}, apply le_antisymm, apply h, apply h, end -- 3ª demostración -- =============== example : min a b = min b a := begin have h : ∀ {x y : ℝ}, min x y ≤ min y x, { intros x y, exact le_min (min_le_right x y) (min_le_left x y) }, exact le_antisymm h h, end -- 4ª demostración -- =============== example : min a b = min b a := begin apply le_antisymm, repeat { apply le_min, apply min_le_right, apply min_le_left }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 19.