Demostrar con Lean4 que si \(α\) es un retículo tal que \[ ∀ 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:
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
Demostrar con Lean4 que en los retículos se verifica que \[ x ⊔ (x ⊓ y) = x \]
Para ello, completar la siguiente teoría de Lean4:
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:
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:
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:
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:
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : x ⊔ y = y ⊔ x := by sorry
Demostrar con Lean4 que en los retículos se verifica que \[x ⊓ y = y ⊓ x\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (x y z : α) example : x ⊓ y = y ⊓ x := by sorry
Demostrar con Lean4 que si \(m, n \in \mathbb{N}\) son números naturales, entonces \[\gcd(m, n) = \gcd(n, m)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (k m n : ℕ) open Nat example : gcd m n = gcd n m := by sorry
Demostrar con Lean4 que si \(x\) divide a \(w\), entonces también divide a \(y(xz)+x^2+w^2\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (w x y z : ℕ) example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by sorry
Demostrar con Lean4 que si \(x, y, z ∈ ℕ\), entonces \(x\) divide a \(yxz\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x y z : ℕ) example : x ∣ y * x * z := by sorry