Demostrar con Lean4 que si \(x, y, z ∈ ℕ\), entonces \(x\) divide a \(yxz\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
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:
|
1 2 3 4 5 6 |
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:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min a b + c = min (a + c) (b + c) := by sorry |
Demostrar con Lean4 que \(a\), \(b\) y \(c\) números reales, entonces \(\min(\min(a, b), c) = \min(a, \min(b, c))\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min (min a b) c = min a (min b c) := by sorry |
Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \(\max(a, b) = \max(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : max a b = max b a := by sorry |