junio 2021 – Calculemus

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]

Intersección con la imagen inversa

PorJosé A. Alonso 21 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,
  split,
  { apply mem_image_of_mem,
    exact hx.1, },
  { rw ← mem_preimage,
    exact hx.2, },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  split,
  { exact mem_image_of_mem f xs, },
  { exact xv, },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  exact ⟨mem_image_of_mem f xs, xv⟩,
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
begin
  rintros x ⟨xs, xv⟩,
  show f x ∈ f '' s ∩ v,
  split,
  { use [x, xs, rfl] },
  { exact xv },
end

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

example : s ∩ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∩ v) :=
inter_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,

split,

{ apply mem_image_of_mem,

exact hx.1, },

{ rw ← mem_preimage,

exact hx.2, },

end

-- 2ª demostración

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

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

begin

rintros x ⟨xs, xv⟩,

split,

{ exact mem_image_of_mem f xs, },

{ exact xv, },

end

-- 3ª demostración

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

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

begin

rintros x ⟨xs, xv⟩,

exact ⟨mem_image_of_mem f xs, xv⟩,

end

-- 4ª demostración

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

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

begin

rintros x ⟨xs, xv⟩,

show f x ∈ f '' s ∩ v,

split,

{ use [x, xs, rfl] },

{ exact xv },

end

-- 5ª demostración

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

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

inter_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 Interseccion_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"
  have "f x ∈ f ` s"
  proof -
    have "x ∈ s"
      using ‹x ∈ s ∩ f -`  v› by (rule IntD1)
    then show "f x ∈ f ` s"
      by (rule imageI)
  qed
  moreover
  have "f x ∈ v"
  proof -
    have "x ∈ f -`  v"
      using ‹x ∈ s ∩ f -`  v› by (rule IntD2)
    then show "f x ∈ v"
      by (rule vimageD)
  qed
  ultimately have "f x ∈ f ` s ∩ v"
    by (rule IntI)
  then show "x ∈ f -` (f ` s ∩ v)"
    by (rule vimageI2)
qed

(* 2ª demostración *)

lemma "s ∩ f -`  v ⊆ f -` (f ` s ∩ v)"
proof (rule subsetI)
  fix x
  assume "x ∈ s ∩ f -`  v"
  have "f x ∈ f ` s"
  proof -
    have "x ∈ s" using ‹x ∈ s ∩ f -`  v› by simp
    then show "f x ∈ f ` s" by simp
  qed
  moreover
  have "f x ∈ v"
  proof -
    have "x ∈ f -`  v" using ‹x ∈ s ∩ f -`  v› by simp
    then show "f x ∈ v" by simp
  qed
  ultimately have "f x ∈ f ` s ∩ v" by simp
  then show "x ∈ f -` (f ` s ∩ v)" by simp
qed

(* 3ª demostración *)

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

end

theory Interseccion_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"

have "f x ∈ f ` s"

proof -

have "x ∈ s"

using ‹x ∈ s ∩ f -` v› by (rule IntD1)

then show "f x ∈ f ` s"

by (rule imageI)

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v"

using ‹x ∈ s ∩ f -` v› by (rule IntD2)

then show "f x ∈ v"

by (rule vimageD)

qed

ultimately have "f x ∈ f ` s ∩ v"

by (rule IntI)

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

by (rule vimageI2)

qed

(* 2ª demostración *)

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

proof (rule subsetI)

fix x

assume "x ∈ s ∩ f -` v"

have "f x ∈ f ` s"

proof -

have "x ∈ s" using ‹x ∈ s ∩ f -` v› by simp

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

qed

moreover

have "f x ∈ v"

proof -

have "x ∈ f -` v" using ‹x ∈ s ∩ f -` v› by simp

then show "f x ∈ v" by simp

qed

ultimately have "f x ∈ f ` s ∩ v" by simp

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

qed

(* 3ª 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]

Unión con la imagen

PorJosé A. Alonso 20 junio 202114 junio 2021

Demostrar que

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

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

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

import data.set.basic
import tactic

open set

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

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

import data.set.basic

import tactic

open set

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

variable f : α → β

variable s : set α

variable v : set β

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

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic
import tactic

open set

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

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  intros y hy,
  cases hy with x hx,
  cases hx with hx1 fxy,
  cases hx1 with xs xv,
  { left,
    use x,
    split,
    { exact xs, },
    { exact fxy, }},
  { right,
    rw ← fxy,
    exact xv, },
end

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  rintros y ⟨x, xs | xv, fxy⟩,
  { left,
    use [x, xs, fxy], },
  { right,
    rw ← fxy,
    exact xv, },
end

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

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
begin
  rintros y ⟨x, xs | xv, fxy⟩;
  finish,
end

import data.set.basic

import tactic

open set

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

variable f : α → β

variable s : set α

variable v : set β

-- 1ª demostración

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

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

begin

intros y hy,

cases hy with x hx,

cases hx with hx1 fxy,

cases hx1 with xs xv,

{ left,

use x,

split,

{ exact xs, },

{ exact fxy, }},

{ right,

rw ← fxy,

exact xv, },

end

-- 2ª demostración

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

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

begin

rintros y ⟨x, xs | xv, fxy⟩,

{ left,

use [x, xs, fxy], },

{ right,

rw ← fxy,

exact xv, },

end

-- 3ª demostración

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

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

begin

rintros y ⟨x, xs | xv, fxy⟩;

finish,

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»]

theory Union_con_la_imagen
imports Main
begin

(* 1ª demostración *)

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
proof (rule subsetI)
  fix y
  assume "y ∈ f ` (s ∪ f -` v)"
  then show "y ∈ f ` s ∪ v"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v"
    proof (rule UnE)
      assume "x ∈ s"
      then have "f x ∈ f ` s"
        by (rule imageI)
      with ‹y = f x› have "y ∈ f ` s"
        by (rule ssubst)
      then show "y ∈ f ` s ∪ v"
        by (rule UnI1)
    next
      assume "x ∈ f -` v"
      then have "f x ∈ v"
        by (rule vimageD)
      with ‹y = f x› have "y ∈ v"
        by (rule ssubst)
      then show "y ∈ f ` s ∪ v"
        by (rule UnI2)
    qed
  qed
qed

(* 2ª demostración *)

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

(* 3ª demostración *)

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
proof
  fix y
  assume "y ∈ f ` (s ∪ f -` v)"
  then show "y ∈ f ` s ∪ v"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v"
    proof
      assume "x ∈ s"
      then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)
    next
      assume "x ∈ f -` v"
      then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)
    qed
  qed
qed

(* 4ª demostración *)

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
proof
  fix y
  assume "y ∈ f ` (s ∪ f -` v)"
  then show "y ∈ f ` s ∪ v"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ s ∪ f -` v"
    then show "y ∈ f ` s ∪ v" using ‹y = f x› by blast
  qed
qed

(* 5ª demostración *)

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

end

100

101

102

103

104

105

theory Union_con_la_imagen

imports Main

begin

(* 1ª demostración *)

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

proof (rule subsetI)

fix y

assume "y ∈ f ` (s ∪ f -` v)"

then show "y ∈ f ` s ∪ v"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof (rule UnE)

assume "x ∈ s"

then have "f x ∈ f ` s"

by (rule imageI)

with ‹y = f x› have "y ∈ f ` s"

by (rule ssubst)

then show "y ∈ f ` s ∪ v"

by (rule UnI1)

assume "x ∈ f -` v"

then have "f x ∈ v"

by (rule vimageD)

with ‹y = f x› have "y ∈ v"

by (rule ssubst)

then show "y ∈ f ` s ∪ v"

by (rule UnI2)

qed

(* 2ª demostración *)

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

proof

fix y

assume "y ∈ f ` (s ∪ f -` v)"

then show "y ∈ f ` s ∪ v"

proof

fix x

assume "y = f x"

assume "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof

assume "x ∈ s"

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

with ‹y = f x› have "y ∈ f ` s" by simp

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

assume "x ∈ f -` v"

then have "f x ∈ v" by simp

with ‹y = f x› have "y ∈ v" by simp

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

qed

(* 3ª demostración *)

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

proof

fix y

assume "y ∈ f ` (s ∪ f -` v)"

then show "y ∈ f ` s ∪ v"

proof

fix x

assume "y = f x"

assume "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v"

proof

assume "x ∈ s"

then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)

assume "x ∈ f -` v"

then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›)

qed

(* 4ª demostración *)

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

proof

fix y

assume "y ∈ f ` (s ∪ f -` v)"

then show "y ∈ f ` s ∪ v"

proof

fix x

assume "y = f x"

assume "x ∈ s ∪ f -` v"

then show "y ∈ f ` s ∪ v" using ‹y = f x› by blast

qed

(* 5ª demostración *)

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

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]