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
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:
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:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : max a b = max b a := by sorry
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \(\min(a, b) = \min(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : min a b = min b a := by sorry
Sean \(a\) y \(b\) números reales. Demostrar con Lean4 que \[|ab| \leq \frac{a^2 + b^2}{2}\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) example : |a * b| \\leq (a ^ 2 + b ^ 2) / 2 := by sorry
Sean \(a\) y \(b\) números reales. Demostrar con Lean4 que \[2ab ≤ a^2 + b^2\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) example : 2*a*b ≤ a^2 + b^2 := by sorry
Sean \(a\), \(b\) y \(c\) números reales. Demostrar con Lean4 que si \(a \leq b\), entonces \[c - e^b \leq c - e^a\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c : ℝ) example (h : a ≤ b) : c - exp b ≤ c - exp a := by sorry
Demostrar con Lean4 que si \(a\) y \(b\) son números reales tales que \(a \leq b\), entonces \[\log(1+e^a) \leq \log(1+e^b)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b : ℝ) example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by sorry