Demostrar con Lean4 que, en los anillos ordenados,
{a≤b,0≤c}⊢ac≤bc
Para ello, completar la siguiente teoría de Lean4:
|
|
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 |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
0≤a–b↔b≤a0≤a→0≤b→0≤ab(a–b)c=ac–bc
Supongamos que
a≤b0≤c
De (1), por L1, se tiene
0≤b–a
y con (2), por L2, se tiene
0≤(b–a)c
que, por L3, da
0≤bc–ac
y, aplicándole L1, se tiene
ac≤bc
Demostraciones con Lean4
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 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by have h3 : 0 ≤ b - a := sub_nonneg.mpr h1 have h4 : 0 ≤ b * c - a * c := calc 0 ≤ (b - a) * c := mul_nonneg h3 h2 _ = b * c - a * c := sub_mul b a c show a * c ≤ b * c exact sub_nonneg.mp h4 -- 2ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by have h3 : 0 ≤ b - a := sub_nonneg.mpr h1 have h4 : 0 ≤ (b - a) * c := mul_nonneg h3 h2 -- h4 : 0 ≤ b * c - a * c rw [sub_mul] at h4 -- a * c ≤ b * c exact sub_nonneg.mp h4 -- 3ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by -- 0 ≤ b * c - a * c apply sub_nonneg.mp -- 0 ≤ (b - a) * c rw [← sub_mul] apply mul_nonneg . -- 0 ≤ b - a exact sub_nonneg.mpr h1 . -- 0 ≤ c exact h2 -- 4ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by apply sub_nonneg.mp rw [← sub_mul] apply mul_nonneg (sub_nonneg.mpr h1) h2 -- 5ª demostración example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := -- by apply? mul_le_mul_of_nonneg_right h1 h2 -- Lemas usados -- ============ -- #check (mul_le_mul_of_nonneg_right : a ≤ b → 0 ≤ c → a * c ≤ b * c) -- #check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b) -- #check (sub_mul a b c : (a - b) * c = a * c - b * c) -- #check (sub_nonneg : 0 ≤ a - b ↔ b ≤ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
