Calculemus

En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

PorJosé A. Alonso 25 agosto 20239 agosto 2023

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

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

En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b

PorJosé A. Alonso 24 agosto 20237 agosto 2023

Demostrar con Lean4 que si \(a\), \(b\) y \(c\) son números reales tales que \(2a \leq 3b\), \(1 \leq a\) y \(c = 2\), entonces \(c + a \leq 5b\).

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

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

example
  (h1 : 2 * a ≤ 3 * b)
  (h2 : 1 ≤ a)
  (h3 : c = 2)
  : c + a ≤ 5 * b :=
sorry

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

example

(h1 : 2 * a ≤ 3 * b)

(h2 : 1 ≤ a)

(h3 : c = 2)

: c + a ≤ 5 * b :=

sorry

En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e

PorJosé A. Alonso 23 agosto 20237 agosto 2023

Demostrar con Lean4 que si \(a\), \(b\), \(c\), \(d\) y \(e\) son números reales tales \(a \leq b\), \(b < c\), \(c \leq d\) y \(d < e\), entonces \(a < e\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
sorry

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

sorry

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

PorJosé A. Alonso 22 agosto 20231 agosto 2023

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

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

sorry

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

PorJosé A. Alonso 21 agosto 20231 agosto 2023

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\) tales que \(ab = 1\) entonces \(a^{-1} = b\).

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

example

(h : a * b = 1)

: a⁻¹ = b :=

sorry