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 |
Demostrar que Si w, x, y, z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w²
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.nat.gcd variables w x y z : ℕ example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := sorry |
Read More «Si w, x, y, z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w²»
Demostrar que si x ∈ ℕ, entonces
|
1 |
x ∣ x^2 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.nat.pow variable x : ℕ example : x ∣ x^2 := sorry |