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
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \[|a| - |b| \leq |a - b|\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| - |b| ≤ |a - b| := by sorry
Demostrar con Lean4 que si \(a\), \(b\) y \(c\) números reales, entonces \[\min(a,b)+c = \min(a+c,b+c)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℝ} example : min a b + c = min (a + c) (b + c) := by sorry