Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces ac ≤ bc
Demostrar que si R es un anillo ordenado y a, b, c ∈ R tales que
|
1 2 |
a ≤ b 0 ≤ c |
entonces
|
1 |
a * c ≤ b * c |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := 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 58 59 60 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin have h3 : 0 ≤ b - a := sub_nonneg.mpr h1, have h4 : 0 ≤ (b - a) * c := mul_nonneg h3 h2, have h5 : (b - a) * c = b * c - a * c := sub_mul b a c, have h6 : 0 ≤ b * c - a * c := eq.trans_ge h5 h4, show a * c ≤ b * c, by exact sub_nonneg.mp h6, end -- 2ª demostración -- =============== open_locale classical example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin by_cases h3 : b ≤ a, { have h3a : a = b := le_antisymm h1 h3, show a * c ≤ b * c, by rw h3a }, { by_cases h4 : c = 0, { calc a * c = a * 0 : by rw h4 ... = 0 : by rw mul_zero ... ≤ 0 : le_refl 0 ... = b * 0 : by rw mul_zero ... = b * c : by {congr ; rw h4}}, { apply le_of_lt, apply mul_lt_mul_of_pos_right, { show a < b, by exact lt_of_le_not_le h1 h3 }, { show 0 < c, by exact lt_of_le_of_ne h2 (ne.symm h4) }}}, end -- 3ª demostración example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := -- by library_search mul_le_mul_of_nonneg_right h1 h2 |
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. 23.