José A. Alonso

Unicidad de inversos en monoides conmutativos

PorJosé A. Alonso 2 julio 202123 junio 2021

Demostrar que en los monoides conmutativos, si un elemento tiene un inverso por la derecha, dicho inverso es único.

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

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
sorry

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : (one_mul y).symm
   ... = (x * z) * y : congr_arg (* y) hz.symm
   ... = (z * x) * y : congr_arg (* y) (mul_comm x z)
   ... = z * (x * y) : mul_assoc z x y
   ... = z * 1       : congr_arg ((*) z) hy
   ... = z           : mul_one z

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp only [one_mul]
   ... = (x * z) * y : by simp only [hz]
   ... = (z * x) * y : by simp only [mul_comm]
   ... = z * (x * y) : by simp only [mul_assoc]
   ... = z * 1       : by simp only [hy]
   ... = z           : by simp only [mul_one]

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp
   ... = (x * z) * y : by simp [hz]
   ... = (z * x) * y : by simp [mul_comm]
   ... = z * (x * y) : by simp [mul_assoc]
   ... = z * 1       : by simp [hy]
   ... = z           : by simp

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
begin
  apply left_inv_eq_right_inv _ hz,
  rw mul_comm,
  exact hy,
end

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
inv_unique hy hz

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

-- 1ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : (one_mul y).symm

... = (x * z) * y : congr_arg (* y) hz.symm

... = (z * x) * y : congr_arg (* y) (mul_comm x z)

... = z * (x * y) : mul_assoc z x y

... = z * 1 : congr_arg ((*) z) hy

... = z : mul_one z

-- 2ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp only [one_mul]

... = (x * z) * y : by simp only [hz]

... = (z * x) * y : by simp only [mul_comm]

... = z * (x * y) : by simp only [mul_assoc]

... = z * 1 : by simp only [hy]

... = z : by simp only [mul_one]

-- 3ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp

... = (x * z) * y : by simp [hz]

... = (z * x) * y : by simp [mul_comm]

... = z * (x * y) : by simp [mul_assoc]

... = z * 1 : by simp [hy]

... = z : by simp

-- 4ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

begin

apply left_inv_eq_right_inv _ hz,

rw mul_comm,

exact hy,

end

-- 5ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

-- 6ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

inv_unique hy hz

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_de_inversos_en_monoides
imports Main
begin

context comm_monoid
begin

(* 1ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by (simp only: left_neutral)
  also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)
  also have "… = (z * x) * y" by (simp only: commute)
  also have "… = z * (x * y)" by (simp only: assoc)
  also have "… = z * 1"       by (simp only: ‹x * y = 1›)
  also have "… = z"           by (simp only: right_neutral)
  finally show "y = z"        by this
qed

(* 2ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by simp
  also have "… = (x * z) * y" using assms(2) by simp
  also have "… = (z * x) * y" by simp
  also have "… = z * (x * y)" by simp
  also have "… = z * 1"       using assms(1) by simp
  also have "… = z"           by simp
  finally show "y = z"        by this
qed

(* 3ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
  using assms
  by auto

end

end

theory Unicidad_de_inversos_en_monoides

imports Main

begin

context comm_monoid

begin

(* 1ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by (simp only: left_neutral)

also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)

also have "… = (z * x) * y" by (simp only: commute)

also have "… = z * (x * y)" by (simp only: assoc)

also have "… = z * 1" by (simp only: ‹x * y = 1›)

also have "… = z" by (simp only: right_neutral)

finally show "y = z" by this

qed

(* 2ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by simp

also have "… = (x * z) * y" using assms(2) by simp

also have "… = (z * x) * y" by simp

also have "… = z * (x * y)" by simp

also have "… = z * 1" using assms(1) by simp

also have "… = z" by simp

finally show "y = z" by this

qed

(* 3ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

using assms

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Equivalencia de inversos iguales al neutro

PorJosé A. Alonso 1 julio 202122 junio 2021

Sea M un monoide y a, b ∈ M tales que a * b = 1. Demostrar que a = 1 si y sólo si b = 1.

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

import algebra.group.basic

variables {M : Type} [monoid M]
variables {a b : M}

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
sorry

import algebra.group.basic

variables {M : Type} [monoid M]

variables {a b : M}

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

variables {M : Type} [monoid M]
variables {a b : M}

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { intro a1,
    rw a1 at h,
    rw one_mul at h,
    exact h, },
  { intro b1,
    rw b1 at h,
    rw mul_one at h,
    exact h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { intro a1,
    calc b = 1 * b : (one_mul b).symm
       ... = a * b : congr_arg (* b) a1.symm
       ... = 1     : h, },
  { intro b1,
    calc a = a * 1 : (mul_one a).symm
       ... = a * b : congr_arg ((*) a) b1.symm
       ... = 1     : h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { rintro rfl,
    simpa using h, },
  { rintro rfl,
    simpa using h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by split ; { rintro rfl, simpa using h }

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by split ; finish

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by finish [iff_def]

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
eq_one_iff_eq_one_of_mul_eq_one h

import algebra.group.basic

variables {M : Type} [monoid M]

variables {a b : M}

-- 1ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ intro a1,

rw a1 at h,

rw one_mul at h,

exact h, },

{ intro b1,

rw b1 at h,

rw mul_one at h,

exact h, },

end

-- 2ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ intro a1,

calc b = 1 * b : (one_mul b).symm

... = a * b : congr_arg (* b) a1.symm

... = 1 : h, },

{ intro b1,

calc a = a * 1 : (mul_one a).symm

... = a * b : congr_arg ((*) a) b1.symm

... = 1 : h, },

end

-- 3ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ rintro rfl,

simpa using h, },

{ rintro rfl,

simpa using h, },

end

-- 4ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by split ; { rintro rfl, simpa using h }

-- 5ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by split ; finish

-- 6ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by finish [iff_def]

-- 7ª demostración

-- ===============

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

eq_one_iff_eq_one_of_mul_eq_one h

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Equivalencia_de_inversos_iguales_al_neutro
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
proof (rule iffI)
  assume "a = 1"
  have "b = 1 * b"      by (simp only: left_neutral)
  also have "… = a * b" by (simp only: ‹a = 1›)
  also have "… = 1"     by (simp only: ‹a * b = 1›)
  finally show "b = 1"  by this
next
  assume "b = 1"
  have "a = a * 1"      by (simp only: right_neutral)
  also have "… = a * b" by (simp only: ‹b = 1›)
  also have "… = 1"     by (simp only: ‹a * b = 1›)
  finally show "a = 1"  by this
qed

(* 2ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
proof
  assume "a = 1"
  have "b = 1 * b"      by simp
  also have "… = a * b" using ‹a = 1› by simp
  also have "… = 1"     using ‹a * b = 1› by simp
  finally show "b = 1"  .
next
  assume "b = 1"
  have "a = a * 1"      by simp
  also have "… = a * b" using ‹b = 1› by simp
  also have "… = 1"     using ‹a * b = 1› by simp
  finally show "a = 1"  .
qed

(* 3ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
  by (metis assms left_neutral right_neutral)

end

end

theory Equivalencia_de_inversos_iguales_al_neutro

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

proof (rule iffI)

assume "a = 1"

have "b = 1 * b" by (simp only: left_neutral)

also have "… = a * b" by (simp only: ‹a = 1›)

also have "… = 1" by (simp only: ‹a * b = 1›)

finally show "b = 1" by this

assume "b = 1"

have "a = a * 1" by (simp only: right_neutral)

also have "… = a * b" by (simp only: ‹b = 1›)

also have "… = 1" by (simp only: ‹a * b = 1›)

finally show "a = 1" by this

qed

(* 2ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

proof

assume "a = 1"

have "b = 1 * b" by simp

also have "… = a * b" using ‹a = 1› by simp

also have "… = 1" using ‹a * b = 1› by simp

finally show "b = 1" .

assume "b = 1"

have "a = a * 1" by simp

also have "… = a * b" using ‹b = 1› by simp

also have "… = 1" using ‹a * b = 1› by simp

finally show "a = 1" .

qed

(* 3ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

by (metis assms left_neutral right_neutral)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Producto de potencias de la misma base en monoides

PorJosé A. Alonso 30 junio 20211 julio 2021

En los monoides se define la
potencia con exponentes naturales por recursión:

   x^0     = 1
   x^(n+1) = x * x^n

1 2	x^0 = 1 x^(n+1) = x * x^n

En Lean la potencia x^n se caracteriza por los siguientes lemas:

   npow_zero' : x ^ 0 = 1
   npow_succ' : x ^ (succ n) = x * x ^ n

1 2	npow_zero' : x ^ 0 = 1 npow_succ' : x ^ (succ n) = x * x ^ n

Demostrar que

    x ^ (m + n) = x ^ m * x ^ n

1	x ^ (m + n) = x ^ m * x ^ n

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

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  x : M
variables (m n : ℕ)

set_option pp.structure_projections false

example :
  x ^ (m + n) = x ^ m * x ^ n :=
sorry

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable x : M

variables (m n : ℕ)

set_option pp.structure_projections false

example :

x ^ (m + n) = x ^ m * x ^ n :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  x : M
variables (m n : ℕ)

-- Para que no use la notación con puntos
set_option pp.structure_projections false

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : congr_arg ((^) x) (nat.zero_add n)
     ... = 1 * x ^ n           : (monoid.one_mul (x ^ n)).symm
     ... = x ^ 0 * x ^ n       : congr_arg (* (x ^ n)) (monoid.npow_zero' x).symm, },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : congr_arg ((^) x) (succ_add m n)
     ... = x * x ^ (m + n)     : pow_succ x (m + n)
     ... = x * (x ^ m * x ^ n) : congr_arg ((*) x) HI
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : congr_arg (* x^n) (pow_succ x m).symm, },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : by simp only [nat.zero_add]
     ... = 1 * x ^ n           : by simp only [monoid.one_mul]
     ... = x ^ 0 * x ^ n       : by simp [monoid.npow_zero'] },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : by simp only [succ_add]
     ... = x * x ^ (m + n)     : by simp only [pow_succ]
     ... = x * (x ^ m * x ^ n) : by simp only [HI]
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : by simp only [pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : by simp [nat.zero_add]
     ... = 1 * x ^ n           : by simp
     ... = x ^ 0 * x ^ n       : by simp, },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : by simp [succ_add]
     ... = x * x ^ (m + n)     : by simp [pow_succ]
     ... = x * (x ^ m * x ^ n) : by simp [HI]
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : by simp [pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { show x ^ (0 + n) = x ^ 0 * x ^ n,
      by simp [nat.zero_add] },
  { show x ^ (succ m + n) = x ^ succ m * x ^ n,
      by finish [succ_add,
                 HI,
                 monoid.mul_assoc,
                 pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
pow_add x m n

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable x : M

variables (m n : ℕ)

-- Para que no use la notación con puntos

set_option pp.structure_projections false

-- 1ª demostración

-- ===============

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : congr_arg ((^) x) (nat.zero_add n)

... = 1 * x ^ n : (monoid.one_mul (x ^ n)).symm

... = x ^ 0 * x ^ n : congr_arg (* (x ^ n)) (monoid.npow_zero' x).symm, },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : congr_arg ((^) x) (succ_add m n)

... = x * x ^ (m + n) : pow_succ x (m + n)

... = x * (x ^ m * x ^ n) : congr_arg ((*) x) HI

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : congr_arg (* x^n) (pow_succ x m).symm, },

end

-- 2ª demostración

-- ===============

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : by simp only [nat.zero_add]

... = 1 * x ^ n : by simp only [monoid.one_mul]

... = x ^ 0 * x ^ n : by simp [monoid.npow_zero'] },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : by simp only [succ_add]

... = x * x ^ (m + n) : by simp only [pow_succ]

... = x * (x ^ m * x ^ n) : by simp only [HI]

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : by simp only [pow_succ], },

end

-- 3ª demostración

-- ===============

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : by simp [nat.zero_add]

... = 1 * x ^ n : by simp

... = x ^ 0 * x ^ n : by simp, },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : by simp [succ_add]

... = x * x ^ (m + n) : by simp [pow_succ]

... = x * (x ^ m * x ^ n) : by simp [HI]

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : by simp [pow_succ], },

end

-- 4ª demostración

-- ===============

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ show x ^ (0 + n) = x ^ 0 * x ^ n,

by simp [nat.zero_add] },

{ show x ^ (succ m + n) = x ^ succ m * x ^ n,

by finish [succ_add,

HI,

monoid.mul_assoc,

pow_succ], },

end

-- 5ª demostración

-- ===============

example :

x ^ (m + n) = x ^ m * x ^ n :=

pow_add x m n

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Producto_de_potencias_de_la_misma_base_en_monoides
imports Main
begin

context monoid_mult
begin

(* 1ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
proof (induct m)
  have "x ^ (0 + n) = x ^ n"                 by (simp only: add_0)
  also have "… = 1 * x ^ n"                 by (simp only: mult_1_left)
  also have "… = x ^ 0 * x ^ n"             by (simp only: power_0)
  finally show "x ^ (0 + n) = x ^ 0 * x ^ n"
    by this
next
  fix m
  assume HI : "x ^ (m + n) = x ^ m * x ^ n"
  have "x ^ (Suc m + n) = x ^ Suc (m + n)"    by (simp only: add_Suc)
  also have "… = x *  x ^ (m + n)"           by (simp only: power_Suc)
  also have "… = x *  (x ^ m * x ^ n)"       by (simp only: HI)
  also have "… = (x *  x ^ m) * x ^ n"       by (simp only: mult_assoc)
  also have "… = x ^ Suc m * x ^ n"          by (simp only: power_Suc)
  finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"
    by this
qed

(* 2ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
proof (induct m)
  have "x ^ (0 + n) = x ^ n"                  by simp
  also have "… = 1 * x ^ n"                  by simp
  also have "… = x ^ 0 * x ^ n"              by simp
  finally show "x ^ (0 + n) = x ^ 0 * x ^ n"
    by this
next
  fix m
  assume HI : "x ^ (m + n) = x ^ m * x ^ n"
  have "x ^ (Suc m + n) = x ^ Suc (m + n)"    by simp
  also have "… = x *  x ^ (m + n)"           by simp
  also have "… = x *  (x ^ m * x ^ n)"       using HI by simp
  also have "… = (x *  x ^ m) * x ^ n"       by (simp add: mult_assoc)
  also have "… = x ^ Suc m * x ^ n"          by simp
  finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"
    by this
qed

(* 3ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
proof (induct m)
  case 0
  then show ?case
    by simp
next
  case (Suc m)
  then show ?case
    by (simp add: algebra_simps)
qed

(* 4ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
  by (induct m) (simp_all add: algebra_simps)

(* 5ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
  by (simp only: power_add)

end

end

theory Producto_de_potencias_de_la_misma_base_en_monoides

imports Main

begin

context monoid_mult

begin

(* 1ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

have "x ^ (0 + n) = x ^ n" by (simp only: add_0)

also have "… = 1 * x ^ n" by (simp only: mult_1_left)

also have "… = x ^ 0 * x ^ n" by (simp only: power_0)

finally show "x ^ (0 + n) = x ^ 0 * x ^ n"

by this

fix m

assume HI : "x ^ (m + n) = x ^ m * x ^ n"

have "x ^ (Suc m + n) = x ^ Suc (m + n)" by (simp only: add_Suc)

also have "… = x * x ^ (m + n)" by (simp only: power_Suc)

also have "… = x * (x ^ m * x ^ n)" by (simp only: HI)

also have "… = (x * x ^ m) * x ^ n" by (simp only: mult_assoc)

also have "… = x ^ Suc m * x ^ n" by (simp only: power_Suc)

finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"

by this

qed

(* 2ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

have "x ^ (0 + n) = x ^ n" by simp

also have "… = 1 * x ^ n" by simp

also have "… = x ^ 0 * x ^ n" by simp

finally show "x ^ (0 + n) = x ^ 0 * x ^ n"

by this

fix m

assume HI : "x ^ (m + n) = x ^ m * x ^ n"

have "x ^ (Suc m + n) = x ^ Suc (m + n)" by simp

also have "… = x * x ^ (m + n)" by simp

also have "… = x * (x ^ m * x ^ n)" using HI by simp

also have "… = (x * x ^ m) * x ^ n" by (simp add: mult_assoc)

also have "… = x ^ Suc m * x ^ n" by simp

finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"

by this

qed

(* 3ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

case 0

then show ?case

by simp

case (Suc m)

then show ?case

by (simp add: algebra_simps)

qed

(* 4ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

by (induct m) (simp_all add: algebra_simps)

(* 5ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

by (simp only: power_add)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

En los monoides, los inversos a la izquierda y a la derecha son iguales

PorJosé A. Alonso 29 junio 202121 junio 2021

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

En Lean, está definida la clase de los monoides (como monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar que si M es un monide, a ∈ M, b es un inverso de a por la izquierda y c es un inverso de a por la derecha, entonce b = c.

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

import algebra.group.defs

variables {M : Type} [monoid M]
variables {a b c : M}

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
sorry

import algebra.group.defs

variables {M : Type} [monoid M]

variables {a b c : M}

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.defs

variables {M : Type} [monoid M]
variables {a b c : M}

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
begin
 rw ←one_mul c,
 rw ←hba,
 rw mul_assoc,
 rw hac,
 rw mul_one b,
end

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b   = b * 1       : (mul_one b).symm
     ... = b * (a * c) : congr_arg (λ x, b * x) hac.symm
     ... = (b * a) * c : (mul_assoc b a c).symm
     ... = 1 * c       : congr_arg (λ x, x * c) hba
     ... = c           : one_mul c

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b   = b * 1       : by finish
     ... = b * (a * c) : by finish
     ... = (b * a) * c : (mul_assoc b a c).symm
     ... = 1 * c       : by finish
     ... = c           : by finish

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
left_inv_eq_right_inv hba hac

import algebra.group.defs

variables {M : Type} [monoid M]

variables {a b c : M}

-- 1ª demostración

-- ===============

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

begin

rw ←one_mul c,

rw ←hba,

rw mul_assoc,

rw hac,

rw mul_one b,

end

-- 2ª demostración

-- ===============

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]

-- 3ª demostración

-- ===============

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

calc b = b * 1 : (mul_one b).symm

... = b * (a * c) : congr_arg (λ x, b * x) hac.symm

... = (b * a) * c : (mul_assoc b a c).symm

... = 1 * c : congr_arg (λ x, x * c) hba

... = c : one_mul c

-- 4ª demostración

-- ===============

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

calc b = b * 1 : by finish

... = b * (a * c) : by finish

... = (b * a) * c : (mul_assoc b a c).symm

... = 1 * c : by finish

... = c : by finish

-- 5ª demostración

-- ===============

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

left_inv_eq_right_inv hba hac

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
proof -
  have      "b  = b ❙* ❙1"      by (simp only: right_neutral)
  also have "… = b ❙* (a ❙* c)" by (simp only: ‹a ❙* c = ❙1›)
  also have "… = (b ❙* a) ❙* c" by (simp only: assoc)
  also have "… = ❙1 ❙* c"       by (simp only: ‹b ❙* a = ❙1›)
  also have "… = c"             by (simp only: left_neutral)
  finally show "b = c"          by this
qed

(* 2ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
proof -
  have      "b  = b ❙* ❙1"      by simp
  also have "… = b ❙* (a ❙* c)" using ‹a ❙* c = ❙1› by simp
  also have "… = (b ❙* a) ❙* c" by (simp add: assoc)
  also have "… = ❙1 ❙* c"       using ‹b ❙* a = ❙1› by simp
  also have "… = c"             by simp
  finally show "b = c"          by this
qed

(* 3ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
  using assms
  by (metis assoc left_neutral right_neutral)

end

end

theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

proof -

have "b = b ❙* ❙1" by (simp only: right_neutral)

also have "… = b ❙* (a ❙* c)" by (simp only: ‹a ❙* c = ❙1›)

also have "… = (b ❙* a) ❙* c" by (simp only: assoc)

also have "… = ❙1 ❙* c" by (simp only: ‹b ❙* a = ❙1›)

also have "… = c" by (simp only: left_neutral)

finally show "b = c" by this

qed

(* 2ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

proof -

have "b = b ❙* ❙1" by simp

also have "… = b ❙* (a ❙* c)" using ‹a ❙* c = ❙1› by simp

also have "… = (b ❙* a) ❙* c" by (simp add: assoc)

also have "… = ❙1 ❙* c" using ‹b ❙* a = ❙1› by simp

also have "… = c" by simp

finally show "b = c" by this

qed

(* 3ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

using assms

by (metis assoc left_neutral right_neutral)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Imagen inversa de la intersección general

PorJosé A. Alonso 27 junio 202118 junio 2021

Demostrar que

   f⁻¹[⋂ i, B(i)] = ⋂ i, f⁻¹[B(i)]

1	f⁻¹[⋂ i, B(i)] = ⋂ i, f⁻¹[B(i)]

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

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables B : I → set β

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
sorry

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables B : I → set β

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables B : I → set β

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  split,
  { intro hx,
    apply mem_Inter_of_mem,
    intro i,
    rw mem_preimage,
    rw mem_preimage at hx,
    rw mem_Inter at hx,
    exact hx i, },
  { intro hx,
    rw mem_preimage,
    rw mem_Inter,
    intro i,
    rw ← mem_preimage,
    rw mem_Inter at hx,
    exact hx i, },
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  calc  (x ∈ f ⁻¹' ⋂ (i : I), B i)
      ↔ f x ∈ ⋂ (i : I), B i       : mem_preimage
  ... ↔ (∀ i : I, f x ∈ B i)       : mem_Inter
  ... ↔ (∀ i : I, x ∈ f ⁻¹' B i)   : iff_of_eq rfl
  ... ↔ x ∈ ⋂ (i : I), f ⁻¹' B i   : mem_Inter.symm,
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
begin
  ext x,
  simp,
end

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by { ext, simp }

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables B : I → set β

-- 1ª demostración

-- ===============

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

split,

{ intro hx,

apply mem_Inter_of_mem,

intro i,

rw mem_preimage,

rw mem_preimage at hx,

rw mem_Inter at hx,

exact hx i, },

{ intro hx,

rw mem_preimage,

rw mem_Inter,

intro i,

rw ← mem_preimage,

rw mem_Inter at hx,

exact hx i, },

end

-- 2ª demostración

-- ===============

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

calc (x ∈ f ⁻¹' ⋂ (i : I), B i)

↔ f x ∈ ⋂ (i : I), B i : mem_preimage

... ↔ (∀ i : I, f x ∈ B i) : mem_Inter

... ↔ (∀ i : I, x ∈ f ⁻¹' B i) : iff_of_eq rfl

... ↔ x ∈ ⋂ (i : I), f ⁻¹' B i : mem_Inter.symm,

end

-- 3ª demostración

-- ===============

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

begin

ext x,

simp,

end

-- 4ª demostración

-- ===============

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=

by { ext, simp }

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_inversa_de_la_interseccion_general
imports Main
begin

(* 1ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof (rule equalityI)
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)"
        using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD)
      then have "f x ∈ B i"
        using ‹i ∈ I› by (rule INT_D)
      then show "x ∈ f -` B i"
        by (rule vimageI2)
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i"
        by (rule INT_D)
      then show "f x ∈ B i"
        by (rule vimageD)
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)"
      by (rule vimageI2)
  qed
qed

(* 2ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume hx : "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp
      then have "f x ∈ B i" using ‹i ∈ I› by simp
      then show "x ∈ f -` B i" by simp
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp
      then show "f x ∈ B i" by simp
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp
  qed
qed

(* 3 demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by (simp only: vimage_INT)

(* 4ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by auto

end

theory Imagen_inversa_de_la_interseccion_general

imports Main

begin

(* 1ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

proof (rule equalityI)

show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"

proof (rule subsetI)

fix x

assume "x ∈ f -` (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. f -` B i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

have "f x ∈ (⋂ i ∈ I. B i)"

using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD)

then have "f x ∈ B i"

using ‹i ∈ I› by (rule INT_D)

then show "x ∈ f -` B i"

by (rule vimageI2)

qed

show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"

proof (rule subsetI)

fix x

assume "x ∈ (⋂ i ∈ I. f -` B i)"

have "f x ∈ (⋂ i ∈ I. B i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i"

by (rule INT_D)

then show "f x ∈ B i"

by (rule vimageD)

qed

then show "x ∈ f -` (⋂ i ∈ I. B i)"

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

proof

show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"

proof (rule subsetI)

fix x

assume hx : "x ∈ f -` (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. f -` B i)"

proof

fix i

assume "i ∈ I"

have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp

then have "f x ∈ B i" using ‹i ∈ I› by simp

then show "x ∈ f -` B i" by simp

qed

show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"

proof

fix x

assume "x ∈ (⋂ i ∈ I. f -` B i)"

have "f x ∈ (⋂ i ∈ I. B i)"

proof

fix i

assume "i ∈ I"

with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp

then show "f x ∈ B i" by simp

qed

then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp

qed

(* 3 demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

by (simp only: vimage_INT)

(* 4ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Imagen inversa de la unión general

PorJosé A. Alonso 26 junio 202116 junio 2021

Demostrar que

   f⁻¹[⋃ i, B i] = ⋃ i, f⁻¹[B i]

1	f⁻¹[⋃ i, B i] = ⋃ i, f⁻¹[B i]

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

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables B : I → set β

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
sorry

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables B : I → set β

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables B : I → set β

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
begin
  ext x,
  split,
  { intro hx,
    rw mem_preimage at hx,
    rw mem_Union at hx,
    cases hx with i fxBi,
    rw mem_Union,
    use i,
    apply mem_preimage.mpr,
    exact fxBi, },
  { intro hx,
    rw mem_preimage,
    rw mem_Union,
    rw mem_Union at hx,
    cases hx with i xBi,
    use i,
    rw mem_preimage at xBi,
    exact xBi, },
end

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
preimage_Union

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by  simp

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables B : I → set β

-- 1ª demostración

-- ===============

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

begin

ext x,

split,

{ intro hx,

rw mem_preimage at hx,

rw mem_Union at hx,

cases hx with i fxBi,

rw mem_Union,

use i,

apply mem_preimage.mpr,

exact fxBi, },

{ intro hx,

rw mem_preimage,

rw mem_Union,

rw mem_Union at hx,

cases hx with i xBi,

use i,

rw mem_preimage at xBi,

exact xBi, },

end

-- 2ª demostración

-- ===============

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

preimage_Union

-- 3ª demostración

-- ===============

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_inversa_de_la_union_general
imports Main
begin

(* 1ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
proof (rule equalityI)
  show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (⋃ i ∈ I. B i)"
    then have "f x ∈ (⋃ i ∈ I. B i)"
      by (rule vimageD)
    then show "x ∈ (⋃ i ∈ I. f -` B i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "f x ∈ B i"
      then have "x ∈ f -` B i"
        by (rule vimageI2)
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋃ i ∈ I. f -` B i)"
    then show "x ∈ f -` (⋃ i ∈ I. B i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ f -` B i"
      then have "f x ∈ B i"
        by (rule vimageD)
      with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)"
        by (rule UN_I)
      then show "x ∈ f -` (⋃ i ∈ I. B i)"
        by (rule vimageI2)
    qed
  qed
qed

(* 2ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
proof
  show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"
  proof
    fix x
    assume "x ∈ f -` (⋃ i ∈ I. B i)"
    then have "f x ∈ (⋃ i ∈ I. B i)" by simp
    then show "x ∈ (⋃ i ∈ I. f -` B i)"
    proof
      fix i
      assume "i ∈ I"
      assume "f x ∈ B i"
      then have "x ∈ f -` B i" by simp
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)" by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"
  proof
    fix x
    assume "x ∈ (⋃ i ∈ I. f -` B i)"
    then show "x ∈ f -` (⋃ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ f -` B i"
      then have "f x ∈ B i" by simp
      with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)" by (rule UN_I)
      then show "x ∈ f -` (⋃ i ∈ I. B i)" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
  by (simp only: vimage_UN)

(* 4ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
  by auto

end

theory Imagen_inversa_de_la_union_general

imports Main

begin

(* 1ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"

proof (rule equalityI)

show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"

proof (rule subsetI)

fix x

assume "x ∈ f -` (⋃ i ∈ I. B i)"

then have "f x ∈ (⋃ i ∈ I. B i)"

by (rule vimageD)

then show "x ∈ (⋃ i ∈ I. f -` B i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "f x ∈ B i"

then have "x ∈ f -` B i"

by (rule vimageI2)

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)"

by (rule UN_I)

qed

show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"

proof (rule subsetI)

fix x

assume "x ∈ (⋃ i ∈ I. f -` B i)"

then show "x ∈ f -` (⋃ i ∈ I. B i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ f -` B i"

then have "f x ∈ B i"

by (rule vimageD)

with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)"

by (rule UN_I)

then show "x ∈ f -` (⋃ i ∈ I. B i)"

by (rule vimageI2)

qed

(* 2ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"

proof

show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"

proof

fix x

assume "x ∈ f -` (⋃ i ∈ I. B i)"

then have "f x ∈ (⋃ i ∈ I. B i)" by simp

then show "x ∈ (⋃ i ∈ I. f -` B i)"

proof

fix i

assume "i ∈ I"

assume "f x ∈ B i"

then have "x ∈ f -` B i" by simp

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)" by (rule UN_I)

qed

show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"

proof

fix x

assume "x ∈ (⋃ i ∈ I. f -` B i)"

then show "x ∈ f -` (⋃ i ∈ I. B i)"

proof

fix i

assume "i ∈ I"

assume "x ∈ f -` B i"

then have "f x ∈ B i" by simp

with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)" by (rule UN_I)

then show "x ∈ f -` (⋃ i ∈ I. B i)" by simp

qed

(* 3ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"

by (simp only: vimage_UN)

(* 4ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Imagen de la intersección general mediante inyectiva

PorJosé A. Alonso 25 junio 202116 junio 2021

Demostrar que si f es inyectiva, entonces

   (⋂ i, f[A i]) ⊆ f[⋂ i, A i]

1	(⋂ i, f[A i]) ⊆ f[⋂ i, A i]

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

import data.set.basic
import tactic

open set function

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : I → set α

example
  (i : I)
  (injf : injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
sorry

import data.set.basic

import tactic

open set function

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : I → set α

example

(i : I)

(injf : injective f)

: (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set function

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : I → set α

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

example
  (i : I)
  (injf : injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
begin
  intros y hy,
  rw mem_Inter at hy,
  rcases hy i with ⟨x, xAi, fxy⟩,
  use x,
  split,
  { apply mem_Inter_of_mem,
    intro j,
    rcases hy j with ⟨z, zAj, fzy⟩,
    convert zAj,
    apply injf,
    rw fxy,
    rw ← fzy, },
  { exact fxy, },
end

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

example
  (i : I)
  (injf : injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
begin
  intro y,
  simp,
  intro h,
  rcases h i with ⟨x, xAi, fxy⟩,
  use x,
  split,
  { intro j,
    rcases h j with ⟨z, zAi, fzy⟩,
    have : f x = f z, by rw [fxy, fzy],
    have : x = z, from injf this,
    rw this,
    exact zAi, },
  { exact fxy, },
end

import data.set.basic

import tactic

open set function

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : I → set α

-- 1ª demostración

-- ===============

example

(i : I)

(injf : injective f)

: (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=

begin

intros y hy,

rw mem_Inter at hy,

rcases hy i with ⟨x, xAi, fxy⟩,

use x,

split,

{ apply mem_Inter_of_mem,

intro j,

rcases hy j with ⟨z, zAj, fzy⟩,

convert zAj,

apply injf,

rw fxy,

rw ← fzy, },

{ exact fxy, },

end

-- 2ª demostración

-- ===============

example

(i : I)

(injf : injective f)

: (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=

begin

intro y,

simp,

intro h,

rcases h i with ⟨x, xAi, fxy⟩,

use x,

split,

{ intro j,

rcases h j with ⟨z, zAi, fzy⟩,

have : f x = f z, by rw [fxy, fzy],

have : x = z, from injf this,

rw this,

exact zAi, },

{ exact fxy, },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Imagen de la intersección general

PorJosé A. Alonso 24 junio 202115 junio 2021

Demostrar que

   f[⋂ i, A i] ⊆ ⋂ i, f[A i]

1	f[⋂ i, A i] ⊆ ⋂ i, f[A i]

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

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : ℕ → set α

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
sorry

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : ℕ → set α

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : ℕ → set α

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intros y h,
  apply mem_Inter_of_mem,
  intro i,
  cases h with x hx,
  cases hx with xIA fxy,
  rw ← fxy,
  apply mem_image_of_mem,
  exact mem_Inter.mp xIA i,
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intros y h,
  apply mem_Inter_of_mem,
  intro i,
  rcases h with ⟨x, xIA, rfl⟩,
  exact mem_image_of_mem f (mem_Inter.mp xIA i),
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
begin
  intro y,
  simp,
  intros x xIA fxy i,
  use [x, xIA i, fxy],
end

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

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=
by tidy

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : ℕ → set α

-- 1ª demostración

-- ===============

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intros y h,

apply mem_Inter_of_mem,

intro i,

cases h with x hx,

cases hx with xIA fxy,

rw ← fxy,

apply mem_image_of_mem,

exact mem_Inter.mp xIA i,

end

-- 2ª demostración

-- ===============

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intros y h,

apply mem_Inter_of_mem,

intro i,

rcases h with ⟨x, xIA, rfl⟩,

exact mem_image_of_mem f (mem_Inter.mp xIA i),

end

-- 3ª demostración

-- ===============

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

begin

intro y,

simp,

intros x xIA fxy i,

use [x, xIA i, fxy],

end

-- 4ª demostración

-- ===============

example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i :=

by tidy

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_de_la_interseccion_general
imports Main
begin

(* 1ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (⋂ i ∈ I. A i)"
  then show "y ∈ (⋂ i ∈ I. f ` A i)"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume xIA : "x ∈ (⋂ i ∈ I. A i)"
    have "f x ∈ (⋂ i ∈ I. f ` A i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with xIA have "x ∈ A i"
        by (rule INT_D)
      then show "f x ∈ f ` A i"
        by (rule imageI)
    qed
    with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)"
      by (rule ssubst)
  qed
qed

(* 2ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
proof
  fix y
  assume "y ∈ f ` (⋂ i ∈ I. A i)"
  then show "y ∈ (⋂ i ∈ I. f ` A i)"
  proof
    fix x
    assume "y = f x"
    assume xIA : "x ∈ (⋂ i ∈ I. A i)"
    have "f x ∈ (⋂ i ∈ I. f ` A i)"
    proof
      fix i
      assume "i ∈ I"
      with xIA have "x ∈ A i" by simp
      then show "f x ∈ f ` A i" by simp
    qed
    with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp
  qed
qed

(* 3ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"
  by auto

end

theory Imagen_de_la_interseccion_general

imports Main

begin

(* 1ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"

proof (rule subsetI)

fix y

assume "y ∈ f ` (⋂ i ∈ I. A i)"

then show "y ∈ (⋂ i ∈ I. f ` A i)"

proof (rule imageE)

fix x

assume "y = f x"

assume xIA : "x ∈ (⋂ i ∈ I. A i)"

have "f x ∈ (⋂ i ∈ I. f ` A i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with xIA have "x ∈ A i"

by (rule INT_D)

then show "f x ∈ f ` A i"

by (rule imageI)

qed

with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)"

by (rule ssubst)

qed

(* 2ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"

proof

fix y

assume "y ∈ f ` (⋂ i ∈ I. A i)"

then show "y ∈ (⋂ i ∈ I. f ` A i)"

proof

fix x

assume "y = f x"

assume xIA : "x ∈ (⋂ i ∈ I. A i)"

have "f x ∈ (⋂ i ∈ I. f ` A i)"

proof

fix i

assume "i ∈ I"

with xIA have "x ∈ A i" by simp

then show "f x ∈ f ` A i" by simp

qed

with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp

qed

(* 3ª demostración *)

lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Imagen de la unión general

PorJosé A. Alonso 23 junio 202115 junio 2021

Demostrar que

   f [⋃ i, A i] = ⋃ i, f [A i]

1	f [⋃ i, A i] = ⋃ i, f [A i]

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

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : ℕ → set α

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
sorry

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : ℕ → set α

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}
variable  f : α → β
variables A : ℕ → set α

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

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
begin
  ext y,
  split,
  { intro hy,
    rw mem_image at hy,
    cases hy with x hx,
    cases hx with xUA fxy,
    rw mem_Union at xUA,
    cases xUA with i xAi,
    rw mem_Union,
    use i,
    rw ← fxy,
    apply mem_image_of_mem,
    exact xAi, },
  { intro hy,
    rw mem_Union at hy,
    cases hy with i yAi,
    cases yAi with x hx,
    cases hx with xAi fxy,
    rw ← fxy,
    apply mem_image_of_mem,
    rw mem_Union,
    use i,
    exact xAi, },
end

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

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
begin
  ext y,
  simp,
  split,
  { rintros ⟨x, ⟨i, xAi⟩, fxy⟩,
    use [i, x, xAi, fxy] },
  { rintros ⟨i, x, xAi, fxy⟩,
    exact ⟨x, ⟨i, xAi⟩, fxy⟩ },
end

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

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
by tidy

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

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
image_Union

import data.set.basic

import tactic

open set

variables {α : Type*} {β : Type*} {I : Type*}

variable f : α → β

variables A : ℕ → set α

-- 1ª demostración

-- ===============

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

begin

ext y,

split,

{ intro hy,

rw mem_image at hy,

cases hy with x hx,

cases hx with xUA fxy,

rw mem_Union at xUA,

cases xUA with i xAi,

rw mem_Union,

use i,

rw ← fxy,

apply mem_image_of_mem,

exact xAi, },

{ intro hy,

rw mem_Union at hy,

cases hy with i yAi,

cases yAi with x hx,

cases hx with xAi fxy,

rw ← fxy,

apply mem_image_of_mem,

rw mem_Union,

use i,

exact xAi, },

end

-- 2ª demostración

-- ===============

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

begin

ext y,

simp,

split,

{ rintros ⟨x, ⟨i, xAi⟩, fxy⟩,

use [i, x, xAi, fxy] },

{ rintros ⟨i, x, xAi, fxy⟩,

exact ⟨x, ⟨i, xAi⟩, fxy⟩ },

end

-- 3ª demostración

-- ===============

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

by tidy

-- 4ª demostración

-- ===============

example : f '' (⋃ i, A i) = ⋃ i, f '' A i :=

image_Union

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Imagen_de_la_union_general
imports Main
begin

(* 1ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"
proof (rule equalityI)
  show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)"
  proof (rule subsetI)
    fix y
    assume "y ∈ f ` (⋃ i ∈ I. A i)"
    then show "y ∈ (⋃ i ∈ I. f ` A i)"
    proof (rule imageE)
      fix x
      assume "y = f x"
      assume "x ∈ (⋃ i ∈ I. A i)"
      then have "f x ∈ (⋃ i ∈ I. f ` A i)"
      proof (rule UN_E)
        fix i
        assume "i ∈ I"
        assume "x ∈ A i"
        then have "f x ∈ f ` A i"
          by (rule imageI)
        with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)"
          by (rule UN_I)
      qed
      with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)"
        by (rule ssubst)
    qed
  qed
next
  show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)"
  proof (rule subsetI)
    fix y
    assume "y ∈ (⋃ i ∈ I. f ` A i)"
    then show "y ∈ f ` (⋃ i ∈ I. A i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "y ∈ f ` A i"
      then show "y ∈ f ` (⋃ i ∈ I. A i)"
      proof (rule imageE)
        fix x
        assume "y = f x"
        assume "x ∈ A i"
        with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)"
          by (rule UN_I)
        then have "f x ∈ f ` (⋃ i ∈ I. A i)"
          by (rule imageI)
        with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)"
          by (rule ssubst)
      qed
    qed
  qed
qed

(* 2ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"
proof
  show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)"
  proof
    fix y
    assume "y ∈ f ` (⋃ i ∈ I. A i)"
    then show "y ∈ (⋃ i ∈ I. f ` A i)"
    proof
      fix x
      assume "y = f x"
      assume "x ∈ (⋃ i ∈ I. A i)"
      then have "f x ∈ (⋃ i ∈ I. f ` A i)"
      proof
        fix i
        assume "i ∈ I"
        assume "x ∈ A i"
        then have "f x ∈ f ` A i" by simp
        with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)" by (rule UN_I)
      qed
      with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)" by simp
    qed
  qed
next
  show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)"
  proof
    fix y
    assume "y ∈ (⋃ i ∈ I. f ` A i)"
    then show "y ∈ f ` (⋃ i ∈ I. A i)"
    proof
      fix i
      assume "i ∈ I"
      assume "y ∈ f ` A i"
      then show "y ∈ f ` (⋃ i ∈ I. A i)"
      proof
        fix x
        assume "y = f x"
        assume "x ∈ A i"
        with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)" by (rule UN_I)
        then have "f x ∈ f ` (⋃ i ∈ I. A i)" by simp
        with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)" by simp
      qed
    qed
  qed
qed

(* 3ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"
  by (simp only: image_UN)

(* 4ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"
  by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

theory Imagen_de_la_union_general

imports Main

begin

(* 1ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"

proof (rule equalityI)

show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)"

proof (rule subsetI)

fix y

assume "y ∈ f ` (⋃ i ∈ I. A i)"

then show "y ∈ (⋃ i ∈ I. f ` A i)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ (⋃ i ∈ I. A i)"

then have "f x ∈ (⋃ i ∈ I. f ` A i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "f x ∈ f ` A i"

by (rule imageI)

with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)"

by (rule UN_I)

qed

with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)"

by (rule ssubst)

qed

show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)"

proof (rule subsetI)

fix y

assume "y ∈ (⋃ i ∈ I. f ` A i)"

then show "y ∈ f ` (⋃ i ∈ I. A i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "y ∈ f ` A i"

then show "y ∈ f ` (⋃ i ∈ I. A i)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ A i"

with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)"

by (rule UN_I)

then have "f x ∈ f ` (⋃ i ∈ I. A i)"

by (rule imageI)

with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)"

by (rule ssubst)

qed

(* 2ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"

proof

show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)"

proof

fix y

assume "y ∈ f ` (⋃ i ∈ I. A i)"

then show "y ∈ (⋃ i ∈ I. f ` A i)"

proof

fix x

assume "y = f x"

assume "x ∈ (⋃ i ∈ I. A i)"

then have "f x ∈ (⋃ i ∈ I. f ` A i)"

proof

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "f x ∈ f ` A i" by simp

with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)" by (rule UN_I)

qed

with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)" by simp

qed

show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)"

proof

fix y

assume "y ∈ (⋃ i ∈ I. f ` A i)"

then show "y ∈ f ` (⋃ i ∈ I. A i)"

proof

fix i

assume "i ∈ I"

assume "y ∈ f ` A i"

then show "y ∈ f ` (⋃ i ∈ I. A i)"

proof

fix x

assume "y = f x"

assume "x ∈ A i"

with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)" by (rule UN_I)

then have "f x ∈ f ` (⋃ i ∈ I. A i)" by simp

with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)" by simp

qed

(* 3ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"

by (simp only: image_UN)

(* 4ª demostración *)

lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Unión con la imagen inversa

PorJosé A. Alonso 22 junio 202115 junio 2021

Demostrar que

   s ∪ f⁻¹[v] ⊆ f¹[f[s] ∪ v]]

1	s ∪ f⁻¹[v] ⊆ f¹[f[s] ∪ v]]

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

import data.set.basic

open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α
variable  v : set β

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

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

variable v : set β

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

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variable  s : set α
variable  v : set β

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  intros x hx,
  rw mem_preimage,
  cases hx with xs xv,
  { apply mem_union_left,
    apply mem_image_of_mem,
    exact xs, },
  { apply mem_union_right,
    rw ← mem_preimage,
    exact xv, },
end

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  intros x hx,
  cases hx with xs xv,
  { apply mem_union_left,
    apply mem_image_of_mem,
    exact xs, },
  { apply mem_union_right,
    exact xv, },
end

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  rintros x (xs | xv),
  { left,
    exact mem_image_of_mem f xs, },
  { right,
    exact xv, },
end

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  rintros x (xs | xv),
  { exact or.inl (mem_image_of_mem f xs), },
  { exact or.inr xv, },
end

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  intros x h,
  exact or.elim h (λ xs, or.inl (mem_image_of_mem f xs)) or.inr,
end

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
λ x h, or.elim h (λ xs, or.inl (mem_image_of_mem f xs)) or.inr

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

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
begin
  rintros x (xs | xv),
  { show f x ∈ f '' s ∪ v,
    use [x, xs, rfl] },
  { show f x ∈ f '' s ∪ v,
    right,
    apply xv },
end

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

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

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variable s : set α

variable v : set β

-- 1ª demostración

-- ===============

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

begin

intros x hx,

rw mem_preimage,

cases hx with xs xv,

{ apply mem_union_left,

apply mem_image_of_mem,

exact xs, },

{ apply mem_union_right,

rw ← mem_preimage,

exact xv, },

end

-- 2ª demostración

-- ===============

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

begin

intros x hx,

cases hx with xs xv,

{ apply mem_union_left,

apply mem_image_of_mem,

exact xs, },

{ apply mem_union_right,

exact xv, },

end

-- 3ª demostración

-- ===============

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

begin

rintros x (xs | xv),

{ left,

exact mem_image_of_mem f xs, },

{ right,

exact xv, },

end

-- 4ª demostración

-- ===============

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

begin

rintros x (xs | xv),

{ exact or.inl (mem_image_of_mem f xs), },

{ exact or.inr xv, },

end

-- 5ª demostración

-- ===============

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

begin

intros x h,

exact or.elim h (λ xs, or.inl (mem_image_of_mem f xs)) or.inr,

end

-- 6ª demostración

-- ===============

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

λ x h, or.elim h (λ xs, or.inl (mem_image_of_mem f xs)) or.inr

-- 7ª demostración

-- ===============

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

begin

rintros x (xs | xv),

{ show f x ∈ f '' s ∪ v,

use [x, xs, rfl] },

{ show f x ∈ f '' s ∪ v,

right,

apply xv },

end

-- 8ª demostración

-- ===============

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

union_preimage_subset s v f

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Union_con_la_imagen_inversa
imports Main
begin

(* 1ª demostración *)

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
proof (rule subsetI)
  fix x
  assume "x ∈ s ∪ f -` v"
  then have "f x ∈ f ` s ∪ v"
  proof (rule UnE)
    assume "x ∈ s"
    then have "f x ∈ f ` s"
      by (rule imageI)
    then show "f x ∈ f ` s ∪ v"
      by (rule UnI1)
  next
    assume "x ∈ f -` v"
    then have "f x ∈ v"
      by (rule vimageD)
    then show "f x ∈ f ` s ∪ v"
      by (rule UnI2)
  qed
  then show "x ∈ f -` (f ` s ∪ v)"
    by (rule vimageI2)
qed

(* 2ª demostración *)

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
proof
  fix x
  assume "x ∈ s ∪ f -` v"
  then have "f x ∈ f ` s ∪ v"
  proof
    assume "x ∈ s"
    then have "f x ∈ f ` s" by simp
    then show "f x ∈ f ` s ∪ v" by simp
  next
    assume "x ∈ f -` v"
    then have "f x ∈ v" by simp
    then show "f x ∈ f ` s ∪ v" by simp
  qed
  then show "x ∈ f -` (f ` s ∪ v)" by simp
qed

(* 3ª demostración *)

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
proof
  fix x
  assume "x ∈ s ∪ f -` v"
  then have "f x ∈ f ` s ∪ v"
  proof
    assume "x ∈ s"
    then show "f x ∈ f ` s ∪ v" by simp
  next
    assume "x ∈ f -` v"
    then show "f x ∈ f ` s ∪ v" by simp
  qed
  then show "x ∈ f -` (f ` s ∪ v)" by simp
qed

(* 4ª demostración *)

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
  by auto

end

theory Union_con_la_imagen_inversa

imports Main

begin

(* 1ª demostración *)

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

proof (rule subsetI)

fix x

assume "x ∈ s ∪ f -` v"

then have "f x ∈ f ` s ∪ v"

proof (rule UnE)

assume "x ∈ s"

then have "f x ∈ f ` s"

by (rule imageI)

then show "f x ∈ f ` s ∪ v"

by (rule UnI1)

assume "x ∈ f -` v"

then have "f x ∈ v"

by (rule vimageD)

then show "f x ∈ f ` s ∪ v"

by (rule UnI2)

qed

then show "x ∈ f -` (f ` s ∪ v)"

by (rule vimageI2)

qed

(* 2ª demostración *)

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

proof

fix x

assume "x ∈ s ∪ f -` v"

then have "f x ∈ f ` s ∪ v"

proof

assume "x ∈ s"

then have "f x ∈ f ` s" by simp

then show "f x ∈ f ` s ∪ v" by simp

assume "x ∈ f -` v"

then have "f x ∈ v" by simp

then show "f x ∈ f ` s ∪ v" by simp

qed

then show "x ∈ f -` (f ` s ∪ v)" by simp

qed

(* 3ª demostración *)

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

proof

fix x

assume "x ∈ s ∪ f -` v"

then have "f x ∈ f ` s ∪ v"

proof

assume "x ∈ s"

then show "f x ∈ f ` s ∪ v" by simp

assume "x ∈ f -` v"

then show "f x ∈ f ` s ∪ v" by simp

qed

then show "x ∈ f -` (f ` s ∪ v)" by simp

qed

(* 4ª demostración *)

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

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]