José A. Alonso

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

PorJosé A. Alonso 26 septiembre 202211 septiembre 2022

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

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ᵇ)

PorJosé A. Alonso 23 septiembre 202211 septiembre 2022

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

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

PorJosé A. Alonso 22 septiembre 202211 septiembre 2022

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

a ≤ b
c < d

1 2	a ≤ b c < d

entonces

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

1	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

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ᵈ

PorJosé A. Alonso 21 septiembre 202211 septiembre 2022

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

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

1 2	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

PorJosé A. Alonso 20 septiembre 202211 septiembre 2022

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

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

a ≤ b

b < c

c ≤ d

d < e

entonces

a < e

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

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⁻¹

PorJosé A. Alonso 19 septiembre 202211 septiembre 2022

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

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

1	(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

import algebra.group

variables {G : Type*} [group G]

variables a b : G

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

sorry

Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b

PorJosé A. Alonso 16 septiembre 202211 septiembre 2022

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

b * a = 1

b * a = 1

entonces

a⁻¹ = b

a⁻¹ = b

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

import algebra.group
variables {G : Type*} [group G]
variables a b : G

example
  (h : b * a = 1)
  : a⁻¹ = b :=
sorry

import algebra.group

variables {G : Type*} [group G]

variables a b : G

example

(h : b * a = 1)

: a⁻¹ = b :=

sorry

Si G es un grupo y a ∈ G, entonces a * 1 = a

PorJosé A. Alonso 15 septiembre 202211 septiembre 2022

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

a * 1 = a

a * 1 = a

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

import algebra.group
variables {G : Type*} [group G]
variables a : G

example : a * 1 = a :=
sorry

import algebra.group

variables {G : Type*} [group G]

variables a : G

example : a * 1 = a :=

sorry

Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1

PorJosé A. Alonso 14 septiembre 202211 septiembre 2022

En Lean, se declara que G es un grupo mediante la expresión

   variables {G : Type*} [group G]

1	variables {G : Type*} [group G]

y, como consecuencia, se tiene los siguientes axiomas

   mul_assoc    : ∀ a b c : G, a * b * c = a * (b * c)
   one_mul      : ∀ a : G,     1 * a = a
   mul_left_inv : ∀ a : G,     a⁻¹ * a = 1

mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

one_mul : ∀ a : G, 1 * a = a

mul_left_inv : ∀ a : G, a⁻¹ * a = 1

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

a * a⁻¹ = 1

1	a * a⁻¹ = 1

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

import algebra.group
variables {G : Type*} [group G]
variables (a b : G)

example : a * a⁻¹ = 1 :=
sorry

import algebra.group

variables {G : Type*} [group G]

variables (a b : G)

example : a * a⁻¹ = 1 :=

sorry

Si R es un anillo y a ∈ R, entonces 2 * a = a + a

PorJosé A. Alonso 13 septiembre 202211 septiembre 2022

Demostrar que si R es un anillo y a ∈ R, entonces

2 * a = a + a.

1	2 * a = a + a.

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

import algebra.ring

variables {R : Type*} [ring R]
variables a : R

example : 2 * a = a + a :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variables a : R

example : 2 * a = a + a :=

sorry