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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

Demostrar con Lean4 que si \(a\), \(c\), \(d\) y \(f\) son números reales tales que \(d ≤ f\), entonces \[c + e^{a + d} \leq c + e^{a + f}\]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a c d f : ℝ)

example
  (h : d ≤ f)
  : c + exp (a + d) ≤ c + exp (a + f) :=
by sorry

Read more…

Demostrar con Lean4 que \(a\), \(b\), \(c\), \(d\) y \(f\) son números reales tales que \(a \leq b\) y \(c < d\), entonces \[a + e^c + f \leq b + e^d + f\]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a b c d f : ℝ)

example
  (h1 : a ≤ b)
  (h2 : c < d)
  : a + exp c + f < b + exp d + f :=
by sorry

Read more…

Demostrar con Lean4 que si \(a\), \(b\) y \(d\) números reales tales que \(1 \leq a\) y \(b \leq d\), entonces \(2 + a + e^b \leq 3a + e^d\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

variable (a b d : ℝ)

example
  (h1 : 1 ≤ a)
  (h2 : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
by sorry

Read more…