Menu Close

Mes: septiembre 2022

Si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ

Demostrar que si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ.

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

import analysis.special_functions.log.basic
import tactic
open real
variables a b c : 
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
sorry

Si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ)

Demostrar que si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ).

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

import analysis.special_functions.log.basic
open real
variables a b : 
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
sorry

Si a, b, c, d, f ∈ ℝ tales que a ≤ b y c < d, entonces a + eᶜ + f < b + eᵈ + f

Demostrar que si a, b, c, d, f ∈ ℝ tales que

a ≤ b
c < d

entonces

a + eᶜ + f < b + eᵈ + f

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

import analysis.special_functions.log.basic
open real
variables a b c d f : 
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
sorry

Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

Demostrar que si a, b, d ∈ ℝ 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 Lean:

import analysis.special_functions.log.basic
open real
variables a b d : 
 
example
  (h  : 1  a)
  (h' : b  d)
  : 2 + a + exp b  3 * a + exp d :=
sorry

Nota: Se pueden usar los lemas

add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d
exp_le_exp : exp a ≤ exp b ↔ a ≤ b

Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e

Demostrar que si a, b, c, d, e ∈ ℝ tales que

a ≤ b
b < c
c ≤ d
d < e

entonces

a < e

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

import data.real.basic
 
variables a b c d e : 
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
sorry

Si G es un grupo y a, b ∈ G, entonces (a * b)⁻¹ = b⁻¹ * a⁻¹

Demostrar que si G es un grupo y a, b ∈ G, entonces

(a * b)⁻¹ = b⁻¹ * a⁻¹

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

import algebra.group
variables {G : Type*} [group G]
variables a b : G
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
sorry