Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a
Demostrar que si R es un anillo ordenado y a b ∈ R, entonces
|
1 |
a ≤ b → 0 ≤ b - a |
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 : a ≤ b → 0 ≤ 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 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R -- 1ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := begin intro h, calc 0 = a - a : (sub_self a).symm ... ≤ b - a : sub_le_sub_right h a end -- 2ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := -- by library_search sub_nonneg.mpr -- 3ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := -- by hint by simp |
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.
