Demostrar con Lean4 que si \(R\) es un retículo tal que \[ (∀ x,\ y,\ z \in α) [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:

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…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…