14 junio 2021 – Calculemus

Imagen inversa de la unión

PorJosé A. Alonso 14 junio 202112 junio 2021

Demostrar que

   f⁻¹[u ∪ v] = f⁻¹[u] ∪ f⁻¹[v]

1	f⁻¹[u ∪ v] = f⁻¹[u] ∪ f⁻¹[v]

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

import data.set.basic

open set

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

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

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

sorry

[expand title=»Soluciones con Lean»]

import data.set.basic

open set

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

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { intros h,
    rw mem_preimage at h,
    cases h with fxu fxv,
    { left,
      apply mem_preimage.mpr,
      exact fxu, },
    { right,
      apply mem_preimage.mpr,
      exact fxv, }},
  { intro h,
    rw mem_preimage,
    cases h with xfu xfv,
    { rw mem_preimage at xfu,
      left,
      exact xfu, },
    { rw mem_preimage at xfv,
      right,
      exact xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { intros h,
    cases h with fxu fxv,
    { left,
      exact fxu, },
    { right,
      exact fxv, }},
  { intro h,
    cases h with xfu xfv,
    { left,
      exact xfu, },
    { right,
      exact xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { rintro (fxu | fxv),
    { exact or.inl fxu, },
    { exact or.inr fxv, }},
  { rintro (xfu | xfv),
    { exact or.inl xfu, },
    { exact or.inr xfv, }},
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  split,
  { finish, },
  { finish, } ,
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
begin
  ext x,
  finish,
end

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by ext; finish

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by ext; refl

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
rfl

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
preimage_union

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=
by simp

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

import data.set.basic

open set

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

variable f : α → β

variables u v : set β

-- 1ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ intros h,

rw mem_preimage at h,

cases h with fxu fxv,

{ left,

apply mem_preimage.mpr,

exact fxu, },

{ right,

apply mem_preimage.mpr,

exact fxv, }},

{ intro h,

rw mem_preimage,

cases h with xfu xfv,

{ rw mem_preimage at xfu,

left,

exact xfu, },

{ rw mem_preimage at xfv,

right,

exact xfv, }},

end

-- 2ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ intros h,

cases h with fxu fxv,

{ left,

exact fxu, },

{ right,

exact fxv, }},

{ intro h,

cases h with xfu xfv,

{ left,

exact xfu, },

{ right,

exact xfv, }},

end

-- 3ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ rintro (fxu | fxv),

{ exact or.inl fxu, },

{ exact or.inr fxv, }},

{ rintro (xfu | xfv),

{ exact or.inl xfu, },

{ exact or.inr xfv, }},

end

-- 4ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

split,

{ finish, },

{ finish, } ,

end

-- 5ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

begin

ext x,

finish,

end

-- 6ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by ext; finish

-- 7ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by ext; refl

-- 8ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

rfl

-- 9ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

preimage_union

-- 10ª demostración

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

example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v :=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]

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

theory Imagen_inversa_de_la_union
imports Main
begin

(* 1ª demostración *)

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

(* 2ª demostración *)

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

(* 3ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
  by (simp only: vimage_Un)

(* 4ª demostración *)

lemma "f -` (u ∪ v) = f -` u ∪ f -` v"
  by auto

end

100

101

102

103

104

105

106

theory Imagen_inversa_de_la_union

imports Main

begin

(* 1ª demostración *)

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

proof (rule equalityI)

show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"

proof (rule subsetI)

fix x

assume "x ∈ f -` (u ∪ v)"

then have "f x ∈ u ∪ v"

by (rule vimageD)

then show "x ∈ f -` u ∪ f -` v"

proof (rule UnE)

assume "f x ∈ u"

then have "x ∈ f -` u"

by (rule vimageI2)

then show "x ∈ f -` u ∪ f -` v"

by (rule UnI1)

assume "f x ∈ v"

then have "x ∈ f -` v"

by (rule vimageI2)

then show "x ∈ f -` u ∪ f -` v"

by (rule UnI2)

qed

show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"

proof (rule subsetI)

fix x

assume "x ∈ f -` u ∪ f -` v"

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

proof (rule UnE)

assume "x ∈ f -` u"

then have "f x ∈ u"

by (rule vimageD)

then have "f x ∈ u ∪ v"

by (rule UnI1)

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

by (rule vimageI2)

assume "x ∈ f -` v"

then have "f x ∈ v"

by (rule vimageD)

then have "f x ∈ u ∪ v"

by (rule UnI2)

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

by (rule vimageI2)

qed

(* 2ª demostración *)

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

proof

show "f -` (u ∪ v) ⊆ f -` u ∪ f -` v"

proof

fix x

assume "x ∈ f -` (u ∪ v)"

then have "f x ∈ u ∪ v" by simp

then show "x ∈ f -` u ∪ f -` v"

proof

assume "f x ∈ u"

then have "x ∈ f -` u" by simp

then show "x ∈ f -` u ∪ f -` v" by simp

assume "f x ∈ v"

then have "x ∈ f -` v" by simp

then show "x ∈ f -` u ∪ f -` v" by simp

qed

show "f -` u ∪ f -` v ⊆ f -` (u ∪ v)"

proof

fix x

assume "x ∈ f -` u ∪ f -` v"

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

proof

assume "x ∈ f -` u"

then have "f x ∈ u" by simp

then have "f x ∈ u ∪ v" by simp

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

assume "x ∈ f -` v"

then have "f x ∈ v" by simp

then have "f x ∈ u ∪ v" by simp

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

qed

(* 3ª demostración *)

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

by (simp only: vimage_Un)

(* 4ª demostración *)

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

by auto

end

[/expand]

[expand title=»Nuevas soluciones»]

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="lean"> (o <pre lang="isar">) y otra con </pre>

[/expand]