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 \(G\) es un grupo y \(a \in G\), entonces \[a·1 = a\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * 1 = a := sorry
En Lean4, se declara que \(G\) es un grupo mediante la expresión
variable {G : Type _} [Group G]
Como consecuencia, se tiene los siguientes axiomas
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) one_mul : ∀ a : G, 1 * a = a mul_left_inv : ∀ a : G, a⁻¹ * a = 1
Demostrar que si \(G\) es un grupo y \(a \in G\), entonces \[aa⁻¹ = 1\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * a⁻¹ = 1 := sorry
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces \[2a = a+a\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a : R) example : 2 * a = a + a := sorry