Imagen de la unión

En Lean, la imagen de un conjunto s por una función f se representa por f '' s; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}

Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t

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

import data.set.basic
import tactic

open set

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
sorry

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

sorry

Soluciones con Lean

import data.set.basic
import tactic

open set

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

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { intro h,
    rw mem_image at h,
    cases h with x hx,
    cases hx with xst fxy,
    rw ← fxy,
    rw mem_union at xst,
    cases xst with xs xt,
    { apply mem_union_left,
      apply mem_image_of_mem,
      exact xs, },
    { apply mem_union_right,
      apply mem_image_of_mem,
      exact xt, }},
  { intro h,
    rw mem_union at h,
    cases h with yfs yft,
    { rw mem_image,
      rw mem_image at yfs,
      cases yfs with x hx,
      cases hx with xs fxy,
      use x,
      split,
      { apply mem_union_left,
        exact xs, },
      { exact fxy, }},
    { rw mem_image,
      rw mem_image at yft,
      cases yft with x hx,
      cases hx with xt fxy,
      use x,
      split,
      { apply mem_union_right,
        exact xt, },
      { exact fxy, }}},
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { rintro ⟨x, xst, rfl⟩,
    cases xst with xs xt,
    { left,
      exact mem_image_of_mem f xs, },
    { right,
      exact mem_image_of_mem f xt, }},
  { rintro (yfs | yft),
    { rcases yfs with ⟨x, xs, rfl⟩,
      apply mem_image_of_mem,
      left,
      exact xs, },
    { rcases yft with ⟨x, xt, rfl⟩,
      apply mem_image_of_mem,
      right,
      exact xt, }},
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { rintro ⟨x, xst, rfl⟩,
    cases xst with xs xt,
    { left,
      use [x, xs], },
    { right,
      use [x, xt], }},
  { rintro (yfs | yft),
    { rcases yfs with ⟨x, xs, rfl⟩,
      use [x, or.inl xs], },
    { rcases yft with ⟨x, xt, rfl⟩,
      use [x, or.inr xt], }},
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { rintro ⟨x, xs | xt, rfl⟩,
    { left,
      use [x, xs], },
    { right,
      use [x, xt], }},
  { rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩),
    { use [x, or.inl xs], },
    { use [x, or.inr xt], }},
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { rintros ⟨x, xs | xt, rfl⟩ ; finish, },
  { rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩) ; finish, },
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  split,
  { finish, },
  { finish, },
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
begin
  ext y,
  rw iff_def,
  finish,
end

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
by finish [ext_iff, iff_def]

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
-- by library_search
image_union f s t

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

import data.set.basic

import tactic

open set

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

variable f : α → β

variables s t : set α

-- 1ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ intro h,

rw mem_image at h,

cases h with x hx,

cases hx with xst fxy,

rw ← fxy,

rw mem_union at xst,

cases xst with xs xt,

{ apply mem_union_left,

apply mem_image_of_mem,

exact xs, },

{ apply mem_union_right,

apply mem_image_of_mem,

exact xt, }},

{ intro h,

rw mem_union at h,

cases h with yfs yft,

{ rw mem_image,

rw mem_image at yfs,

cases yfs with x hx,

cases hx with xs fxy,

use x,

split,

{ apply mem_union_left,

exact xs, },

{ exact fxy, }},

{ rw mem_image,

rw mem_image at yft,

cases yft with x hx,

cases hx with xt fxy,

use x,

split,

{ apply mem_union_right,

exact xt, },

{ exact fxy, }}},

end

-- 2ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ rintro ⟨x, xst, rfl⟩,

cases xst with xs xt,

{ left,

exact mem_image_of_mem f xs, },

{ right,

exact mem_image_of_mem f xt, }},

{ rintro (yfs | yft),

{ rcases yfs with ⟨x, xs, rfl⟩,

apply mem_image_of_mem,

left,

exact xs, },

{ rcases yft with ⟨x, xt, rfl⟩,

apply mem_image_of_mem,

right,

exact xt, }},

end

-- 3ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ rintro ⟨x, xst, rfl⟩,

cases xst with xs xt,

{ left,

use [x, xs], },

{ right,

use [x, xt], }},

{ rintro (yfs | yft),

{ rcases yfs with ⟨x, xs, rfl⟩,

use [x, or.inl xs], },

{ rcases yft with ⟨x, xt, rfl⟩,

use [x, or.inr xt], }},

end

-- 4ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ rintro ⟨x, xs | xt, rfl⟩,

{ left,

use [x, xs], },

{ right,

use [x, xt], }},

{ rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩),

{ use [x, or.inl xs], },

{ use [x, or.inr xt], }},

end

-- 5ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ rintros ⟨x, xs | xt, rfl⟩ ; finish, },

{ rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩) ; finish, },

end

-- 6ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

split,

{ finish, },

end

-- 7ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

begin

ext y,

rw iff_def,

finish,

end

-- 8ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

by finish [ext_iff, iff_def]

-- 9ª demostración

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=

-- by library_search

image_union f s t

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Imagen_de_la_union
imports Main
begin

section ‹1ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"
proof (rule equalityI)
  show "f ` (s ∪ t) ⊆ f ` s ∪ f ` t"
  proof (rule subsetI)
    fix y
    assume "y ∈ f ` (s ∪ t)"
    then show "y ∈ f ` s ∪ f ` t"
    proof (rule imageE)
      fix x
      assume "y = f x"
      assume "x ∈ s ∪ t"
      then show "y ∈ f ` s ∪ f ` t"
      proof (rule UnE)
        assume "x ∈ s"
        with ‹y = f x› have "y ∈ f ` s"
          by (simp only: image_eqI)
        then show "y ∈ f ` s ∪ f ` t"
          by (rule UnI1)
      next
        assume "x ∈ t"
        with ‹y = f x› have "y ∈ f ` t"
          by (simp only: image_eqI)
        then show "y ∈ f ` s ∪ f ` t"
          by (rule UnI2)
      qed
    qed
  qed
next
  show "f ` s ∪ f ` t ⊆ f ` (s ∪ t)"
  proof (rule subsetI)
    fix y
    assume "y ∈ f ` s ∪ f ` t"
    then show "y ∈ f ` (s ∪ t)"
    proof (rule UnE)
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∪ t)"
      proof (rule imageE)
        fix x
        assume "y = f x"
        assume "x ∈ s"
        then have "x ∈ s ∪ t"
          by (rule UnI1)
        with ‹y = f x› show "y ∈ f ` (s ∪ t)"
          by (simp only: image_eqI)
      qed
    next
      assume "y ∈ f ` t"
      then show "y ∈ f ` (s ∪ t)"
      proof (rule imageE)
        fix x
        assume "y = f x"
        assume "x ∈ t"
        then have "x ∈ s ∪ t"
          by (rule UnI2)
        with ‹y = f x› show "y ∈ f ` (s ∪ t)"
          by (simp only: image_eqI)
      qed
    qed
  qed
qed

section ‹2ª demostración›

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

section ‹3ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"
  by (simp only: image_Un)

section ‹4ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"
  by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

theory Imagen_de_la_union

imports Main

begin

section ‹1ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"

proof (rule equalityI)

show "f ` (s ∪ t) ⊆ f ` s ∪ f ` t"

proof (rule subsetI)

fix y

assume "y ∈ f ` (s ∪ t)"

then show "y ∈ f ` s ∪ f ` t"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s ∪ t"

then show "y ∈ f ` s ∪ f ` t"

proof (rule UnE)

assume "x ∈ s"

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

by (simp only: image_eqI)

then show "y ∈ f ` s ∪ f ` t"

by (rule UnI1)

assume "x ∈ t"

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

by (simp only: image_eqI)

then show "y ∈ f ` s ∪ f ` t"

by (rule UnI2)

qed

show "f ` s ∪ f ` t ⊆ f ` (s ∪ t)"

proof (rule subsetI)

fix y

assume "y ∈ f ` s ∪ f ` t"

then show "y ∈ f ` (s ∪ t)"

proof (rule UnE)

assume "y ∈ f ` s"

then show "y ∈ f ` (s ∪ t)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ s ∪ t"

by (rule UnI1)

with ‹y = f x› show "y ∈ f ` (s ∪ t)"

by (simp only: image_eqI)

qed

assume "y ∈ f ` t"

then show "y ∈ f ` (s ∪ t)"

proof (rule imageE)

fix x

assume "y = f x"

assume "x ∈ t"

then have "x ∈ s ∪ t"

by (rule UnI2)

with ‹y = f x› show "y ∈ f ` (s ∪ t)"

by (simp only: image_eqI)

qed

section ‹2ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"

proof

show "f ` (s ∪ t) ⊆ f ` s ∪ f ` t"

proof

fix y

assume "y ∈ f ` (s ∪ t)"

then show "y ∈ f ` s ∪ f ` t"

proof

fix x

assume "y = f x"

assume "x ∈ s ∪ t"

then show "y ∈ f ` s ∪ f ` t"

proof

assume "x ∈ s"

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

by simp

then show "y ∈ f ` s ∪ f ` t"

by simp

assume "x ∈ t"

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

by simp

then show "y ∈ f ` s ∪ f ` t"

by simp

qed

show "f ` s ∪ f ` t ⊆ f ` (s ∪ t)"

proof

fix y

assume "y ∈ f ` s ∪ f ` t"

then show "y ∈ f ` (s ∪ t)"

proof

assume "y ∈ f ` s"

then show "y ∈ f ` (s ∪ t)"

proof

fix x

assume "y = f x"

assume "x ∈ s"

then have "x ∈ s ∪ t"

by simp

with ‹y = f x› show "y ∈ f ` (s ∪ t)"

by simp

qed

assume "y ∈ f ` t"

then show "y ∈ f ` (s ∪ t)"

proof

fix x

assume "y = f x"

assume "x ∈ t"

then have "x ∈ s ∪ t"

by simp

with ‹y = f x› show "y ∈ f ` (s ∪ t)"

by simp

qed

section ‹3ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"

by (simp only: image_Un)

section ‹4ª demostración›

lemma "f ` (s ∪ t) = f ` s ∪ f ` t"

by auto

end

Share this:

Escribe un comentarioCancel reply