Skip to main content

En ℝ, (cb)a = b(ac)

Números reales

Demostrar con Lean4 que los números reales tienen la siguiente propiedad \[ (cb)a = b(ac) \]

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (c * b) * a = b * (a * c) :=
by sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades: \begin{align} (cb)a &= (bc)a &&\text{[por la conmutativa]} \newline &= b(ca) &&\text{[por la asociativa]} \newline &= b(ac) &&\text{[por la conmutativa]} \end{align}

Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- 1ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
calc
  (c * b) * a
    = (b * c) * a := by rw [mul_comm c b]
  _ = b * (c * a) := by rw [mul_assoc]
  _ = b * (a * c) := by rw [mul_comm c a]

-- 2ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
by
  rw [mul_comm c b]
  rw [mul_assoc]
  rw [mul_comm c a]

-- 3ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
by ring

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

En ℝ, (ab)c = b(ac)

Números reales

Demostrar con Lean4 que los números reales tienen la siguiente propiedad \[ (ab)c = b(ac) \]

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades \begin{align} (ab)c &= (ba)c &&\text{[por la conmutativa]} \newline &= b(ac) &&\text{[por la asociativa]} \end{align}

Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- 1ª demostración
example
  (a b c : ℝ)
  : (a * b) * c = b * (a * c) :=
calc
  (a * b) * c = (b * a) * c := by rw [mul_comm a b]
            _ = b * (a * c) := by rw [mul_assoc b a c]

-- 2ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

-- 3ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
by ring

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

El producto por un par es par

Números naturales

Demostrar que los productos de los números naturales por números pares son pares.

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

import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic

open Nat

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  sorry

Demostración en lenguaje natural

Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que \[ \begin{align} n = k + k && (1) \end{align} \] Por tanto, \[ \begin{align} mn &= m(k + k) && (\text{por (1)})\newline &= mk + mk && (\text{por la propiedad distributiva}) \end{align} \] Por consiguiente, \(mn\) es par.

Soluciones con Lean4

import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic

open Nat

-- 1ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  ring

-- 2ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  rw [mul_add]

-- 3ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk, mul_add]

-- 4ª demostración
-- ===============

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add]

-- 5ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  exact ⟨m * k, by rw [hk, mul_add]⟩

-- 6ª demostración
-- ===============

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

-- 7ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  exact mul_add m k k

-- 8ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    rw [hk, mul_add]

-- 9ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    calc m * n
       = m * (k + k)   := by exact congrArg (HMul.hMul m) hk
     _ = m * k + m * k := by exact mul_add m k k

-- 10ª demostración
-- ================

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

-- Lemas usados
-- ============

-- #check (mul_add : ∀ a b c : ℕ, a * (b + c) = a * b + a * c)

Se puede interactuar con las pruebas anteriores en Lean 4 Web.

Referencias

Demostraciones de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \]

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

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen_inversa
imports Main
begin

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
sorry

end

Read more…

Intersección con la imagen

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen_inversa
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s] ∩ t = f[s ∩ f⁻¹[t]]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (t : Set β)

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus t] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

lemma "f ` s - f ` t ⊆ f ` (s - t)"
sorry

end

Read more…

Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

Funciones

Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es inyectiva, entonces \[ f[s] ∩ f[t] ⊆ f[s ∩ t] \]

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

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example
  (h : Injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas
imports Main
begin

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
sorry

end

Read more…

Demostraciones de "f[s ∩ t] ⊆ f[s] ∩ f[t]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∩ t] ⊆ f[s] ∩ f[t]​ \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion
imports Main
begin

lemma "f ` (s ∩ t) ⊆ f ` s ∩ f ` t"
sorry

end

Read more…

Demostraciones de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\]

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

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}
variable (f : α → β)
variable (A B : Set β)

example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B :=
by sorry

y la siguiente teoría de IsabelleHOL:

theory Imagen_inversa_de_la_union
imports Main
begin

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
sorry

end

Read more…