Demostrar con Lean4 que, en los anillos ordenados,
\[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by sorry |
Read More «En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc»
Demostrar con Lean4 que en los anillos ordenados
\[ 0 ≤ b – a → a ≤ b \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : 0 ≤ b - a → a ≤ b := by sorry |
Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : a ≤ b → 0 ≤ b - a := by sorry |
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
Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces
|
1 |
0 ≤ b - a → a ≤ b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : 0 ≤ b - a → a ≤ b := sorry |
Read More «Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b»