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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

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

Read more…

Demostrar con Lean4 que si \(R\) es un anillo y \(a, b \in R\), entonces \[a - b = a + -b\]

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a b : R)

example : a - b = a + -b :=
sorry

Read more…

Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces \[ -(-a) = a \]

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

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic

variable {R : Type _} [Ring R]
variable {a : R}

example : -(-a) = a :=
sorry

Read more…

Demostrar con Lean4 que si R es un anillo, entonces \[ -0 = 0 \]

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

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic

variable {R : Type _} [Ring R]

example : (-0 : R) = 0 :=
sorry

Read more…