José A. AlonsoDemostrar que si X es un espacio métrico y x, y ∈ X, entonces
0 ≤ dist x y |
Para ello, completar la siguiente teoría de Lean:
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X example : 0 ≤ dist x y := sorry |
Demostrar que si R es un anillo ordenado y a, b, c ∈ R tales que
a ≤ b 0 ≤ c |
entonces
a * c ≤ b * c |
Para ello, completar la siguiente teoría de Lean:
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
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.
Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces
0 ≤ b - a → a ≤ b |
Para ello, completar la siguiente teoría de Lean:
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : 0 ≤ b - a → a ≤ b := sorry |
Demostrar que si R es un anillo ordenado y a b ∈ R, entonces
a ≤ b → 0 ≤ b - a |
Para ello, completar la siguiente teoría de Lean:
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : a ≤ b → 0 ≤ b - a := sorry |
Demostrar que Si R es un retículo tal que
∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) |
entonces
∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := sorry |
Demostrar que si R es un retículo tal que
(∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))), |
entonces
(∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)) |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := sorry |
Demostrar que si R es un retículo y x, y ∈ R, entonces
x ⊔ (x ⊓ y) = x |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊔ (x ⊓ y) = x := sorry |
Demostrar que si R es un retículo y x, y ∈ R, entonces
x ⊓ (x ⊔ y) = x |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊓ (x ⊔ y) = x := sorry |
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := sorry |
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) |
Para ello, completar la siguiente teoría de Lean:
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := sorry |