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 |
Read More «Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a»
Demostrar que Si R es un retículo tal que
|
1 |
∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) |
entonces
|
1 |
∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
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
|
1 |
(∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))), |
entonces
|
1 |
(∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
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
|
1 |
x ⊔ (x ⊓ y) = x |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊔ (x ⊓ y) = x := sorry |
Read More «Si R es un retículo y x, y ∈ R, entonces x ⊔ (x ⊓ y) = x»
Demostrar que si R es un retículo y x, y ∈ R, entonces
|
1 |
x ⊓ (x ⊔ y) = x |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊓ (x ⊔ y) = x := sorry |
Read More «Si R es un retículo y x, y ∈ R, entonces x ⊓ (x ⊔ y) = x»
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
|
1 |
(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) := sorry |
Read More «Si R es un retículo y x, y, z ∈ R, entonces (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)»
Demostrar que si R es un retículo y x, y, z ∈ R, entonces
|
1 |
(x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y z : R example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) := sorry |
Read More «Si R es un retículo y x, y, z ∈ R, entonces (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)»
Demostrar que si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊔ y = y ⊔ x := sorry |
Read More «Si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x»
Sea R un retículo. Demostrar que si x, y ∈ R, entonces
|
1 |
x ⊓ y = y ⊓ x |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] variables x y : R example : x ⊓ y = y ⊓ x := sorry |
Read More «Si R es un retículo y x, y ∈ R, entonces x ⊓ y = y ⊓ x»
Demostrar que si m, n ∈ ℕ, entonces gcd(m,n) = gcd(n,m).
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.nat.gcd open nat variables k m n : ℕ example : gcd m n = gcd n m := sorry |