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 con Lean4 que si \(R\) es un retículo tal que
\[ (∀ x,\ y,\ z \in R) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \]
entonces
\[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \]
para todos los elementos del retículo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := by sorry |
Read More «En los retículos, una distributiva del supremo implica la otra»
Demostrar con Lean4 que si α es un retículo tal que se
$$(∀ x, y, z) [x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))]$$
entonces
$$(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$$
para todos los elementos de α.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := by sorry |
Read More «En los retículos, una distributiva del ínfimo implica la otra»
Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊔ (x ⊓ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α]-- variable (x y : α) example : x ⊔ (x ⊓ y) = x := by sorry |
Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊓ (x ⊔ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y : α) example : x ⊓ (x ⊔ y) = x := by sorry |
Demostrar con Lean4 que en los retículos se verifica que
\[ (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := by sorry |
Demostrar con Lean4 que en los retículos se verifica que
\[(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := by sorry |
Demostrar con Lean4 que en los retículos se verifica que
\[x ⊔ y = y ⊔ x\]
para todo \(x\) e \(y\) en el retículo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : x ⊔ y = y ⊔ x := by sorry |