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:
|
1 2 3 4 5 6 7 8 9 10 |
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:
|
1 2 3 4 5 6 7 8 |
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 «En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)»
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:
|
1 2 3 4 5 6 7 8 |
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 «En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)»
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:
|
1 2 3 4 5 6 7 8 9 |
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 «En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f"
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:
|
1 2 3 4 5 6 7 8 9 10 11 |
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 «En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ»
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:
|
1 2 3 4 5 6 7 8 9 10 |
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 |
Read More «En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b»
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:
|
1 2 3 4 5 6 7 8 9 10 11 |
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 |
Read More «En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e"
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:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry |
Read More «Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹»
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:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example (h : a * b = 1) : a⁻¹ = b := sorry |
Read More «Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b»
Demostrar con Lean4 que si \(G\) es un grupo y \(a \in G\), entonces
\[a·1 = a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * 1 = a := sorry |