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
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
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
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 import Mathlib.Tactic variable (a b c : ℝ) example (h1 : 2 * a ≤ 3 * b) (h2 : 1 ≤ a) (h3 : c = 2) : c + a ≤ 5 * b := sorry
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 import Mathlib.Tactic variable (a b c d e : ℝ) example (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) (h4 : d < e) : a < e := sorry
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:
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * 1 = a := sorry
En Lean4, se declara que \(G\) es un grupo mediante la expresión
variable {G : Type _} [Group G]
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
Demostrar que si \(G\) es un grupo y \(a \in G\), entonces \[aa⁻¹ = 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 * a⁻¹ = 1 := sorry
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces \[2a = a+a\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Defs variable {R : Type _} [Ring R] variable (a : R) example : 2 * a = a + a := sorry
Demostrar con Lean4 que En los anillos, \(1 + 1 = 2\)
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] example : 1 + 1 = (2 : R) := sorry
Demostrar con Lean4 que si \(R\) es un anillo y \(a \in R\), entonces \[a - a = 0\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Defs import Mathlib.Algebra.Group.Basic variable {R : Type _} [Ring R] variable (a : R) example : a - a = 0 := sorry