Skip to main content

Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

Órdenes parciales

Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a ≤ b\), entonces \(b\) es una cota superior de \(s\).

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry

Read more…

Si r ⊆ s y s ⊆ t, entonces r ⊆ t

Conjuntos

Demostrar con Lean4 que si \(r ⊆ s\) y \(s ⊆ t\), entonces \(r ⊆ t\).

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

import Mathlib.Tactic

open Set

variable {α : Type _}
variable (r s t : Set α)

example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
by sorry

Read more…

Para cualquier conjunto s, s ⊆ s

Conjuntos

Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).

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

import Mathlib.Tactic

variable {α : Type _}
variable (s : Set α)

example : s ⊆ s :=
by sorry

Read more…

Si f es par y g es impar, entonces (f ∘ g) es par

Funciones reales

Demostrar con Lean4 que si \(f\) es par y \(g\) es impar, entonces \(f ∘ g\) es par.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

-- (esImpar f) expresa que f es impar.
def esImpar  (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = - f (-x)

example
  (h1 : esPar f)
  (h2 : esImpar g)
  : esPar (f ∘ g) :=
by sorry

Read more…

El producto de una función par por una impar es impar

Funciones reales

Demostrar con Lean4 que el producto de una función par por una impar es impar.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

-- (esImpar f) expresa que f es impar.
def esImpar  (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = - f (-x)

example
  (h1 : esPar f)
  (h2 : esImpar g)
  : esImpar (f * g) :=
by sorry

Read more…

El producto de dos funciones impares es par

Funciones reales

Demostrar con Lean4 que el producto de dos funciones impares es par.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

-- (esImpar f) expresa que f es impar.
def esImpar  (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = - f (-x)

example
  (h1 : esImpar f)
  (h2 : esImpar g)
  : esPar (f * g) :=
by sorry

Read more…

La suma de dos funciones pares es par

Funciones reales

Demostrar con Lean4 que la suma de dos funciones pares es par.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

example
  (h1 : esPar f)
  (h2 : esPar g)
  : esPar (f + g) :=
by sorry

Read more…

Si c es no negativo y f es monótona, entonces cf es monótona.

Funciones reales

Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.

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

import Mathlib.Data.Real.Basic

variable (f : ℝ → ℝ)
variable {c : ℝ}

example
  (mf : Monotone f)
  (nnc : 0 ≤ c)
  : Monotone (fun x ↦ c * f x) :=
by sorry

Read more…

La suma de dos funciones monótonas es monótona

Funciones reales

Demostrar con Lean4 que la suma de dos funciones monótonas es monótona.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f + g) :=
by sorry

Read more…