f[s] ∩ t = f[s ∩ f⁻¹[t]]

Demostrar con Lean4 que
\[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]

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

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

open Set

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

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

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s : Set α)

variable (t : Set β)

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

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que, para toda \(y\),
\[ y ∈ f[s] ∩ t ↔ y ∈ f[s ∩ f⁻¹[t]] \]
Lo haremos probando las dos implicaciones.

(⟹) Supongamos que \(y ∈ f[s] ∩ t\). Entonces, se tiene que
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∈ t \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
Por (2) y (4),
\[ f(x) ∈ t \]
y, por tanto,
\[ x ∈ f⁻¹[t] \]
que, junto con (3), da
\{ x ∈ s ∩ f⁻¹[t] \]
y, por tanto,
\[ f(x) ∈ f[s ∩ f⁻¹[t]] \]
que, junto con (4), da
\[ y ∈ f[s ∩ f⁻¹[t]] \]

(⟸) Supongamos que \(y ∈ f[s ∩ f⁻¹[t]]\). Entonces, existe un \(x\) tal que
\begin{align}
&x ∈ s ∩ f⁻¹[t] \tag{5} \\
&f(x) = y \tag{6}
\end{align}
Por (1), se tiene que
\begin{align}
&x ∈ s \tag{7} \\
&x ∈ f⁻¹[t] \tag{8}
\end{align}
Por (7) se tiene que
\[ f(x) ∈ f[s] \]
y, junto con (6), se tiene que
\[ y ∈ f[s] \tag{9} \]
Por (8), se tiene que
\[ f(x) ∈ t \]
y, junto con (6), se tiene que
\[ y ∈ t \tag{10} \]
Por (9) y (19), se tiene que
\[ y ∈ f[s] ∩ t \]

2. Demostraciones con Lean4

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

open Set

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

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by
  ext y
  -- y : β
  -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
  have h1 : y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) := by
    intro hy
    -- hy : y ∈ f '' s ∩ t
    -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)
    have h1a : y ∈ f '' s := hy.1
    obtain ⟨x : α, hx: x ∈ s ∧ f x = y⟩ := h1a
    have h1b : x ∈ s := hx.1
    have h1c : f x = y := hx.2
    have h1d : y ∈ t := hy.2
    have h1e : f x ∈ t := by rwa [←h1c] at h1d
    have h1f : x ∈ s ∩ f ⁻¹' t := mem_inter h1b h1e
    have h1g : f x ∈ f '' (s ∩ f ⁻¹' t) := mem_image_of_mem f h1f
    show y ∈ f '' (s ∩ f ⁻¹' t)
    rwa [h1c] at h1g
  have h2 : y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t :=  by
    intro hy
    -- hy : y ∈ f '' (s ∩ f ⁻¹' t)
    -- ⊢ y ∈ f '' s ∩ t
    obtain ⟨x : α, hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y⟩ := hy
    have h2a : x ∈ s := hx.1.1
    have h2b : f x ∈ f '' s := mem_image_of_mem f h2a
    have h2c : y ∈ f '' s := by rwa [hx.2] at h2b
    have h2d : x ∈ f ⁻¹' t := hx.1.2
    have h2e : f x ∈ t := mem_preimage.mp h2d
    have h2f : y ∈ t := by rwa [hx.2] at h2e
    show y ∈ f '' s ∩ t
    exact mem_inter h2c h2f
  show y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
  exact ⟨h1, h2⟩

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by
  ext y
  -- y : β
  -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
  constructor
  . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)
    intro hy
    -- hy : y ∈ f '' s ∩ t
    -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)
    cases' hy with hyfs yt
    -- hyfs : y ∈ f '' s
    -- yt : y ∈ t
    cases' hyfs with x hx
    -- x : α
    -- hx : x ∈ s ∧ f x = y
    cases' hx with xs fxy
    -- xs : x ∈ s
    -- fxy : f x = y
    use x
    -- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y
    constructor
    . -- ⊢ x ∈ s ∩ f ⁻¹' t
      constructor
      . -- ⊢ x ∈ s
        exact xs
      . -- ⊢ x ∈ f ⁻¹' t
        rw [mem_preimage]
        -- ⊢ f x ∈ t
        rw [fxy]
        -- ⊢ y ∈ t
        exact yt
    . -- ⊢ f x = y
      exact fxy
  . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t
    intro hy
    -- hy : y ∈ f '' (s ∩ f ⁻¹' t)
    -- ⊢ y ∈ f '' s ∩ t
    cases' hy with x hx
    -- x : α
    -- hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y
    constructor
    . -- ⊢ y ∈ f '' s
      use x
      -- ⊢ x ∈ s ∧ f x = y
      constructor
      . -- ⊢ x ∈ s
        exact hx.1.1
      . -- ⊢ f x = y
        exact hx.2
    . -- ⊢ y ∈ t
      cases' hx with hx1 fxy
      -- hx1 : x ∈ s ∩ f ⁻¹' t
      -- fxy : f x = y
      rw [←fxy]
      -- ⊢ f x ∈ t
      rw [←mem_preimage]
      -- ⊢ x ∈ f ⁻¹' t
      exact hx1.2

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by
  ext y
  -- y : β
  -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
  constructor
  . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)
    rintro ⟨⟨x, xs, fxy⟩, yt⟩
    -- yt : y ∈ t
    -- x : α
    -- xs : x ∈ s
    -- fxy : f x = y
    -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)
    use x
    -- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y
    constructor
    . -- ⊢ x ∈ s ∩ f ⁻¹' t
      constructor
      . -- ⊢ x ∈ s
        exact xs
      . -- ⊢ x ∈ f ⁻¹' t
        rw [mem_preimage]
        -- ⊢ f x ∈ t
        rw [fxy]
        -- ⊢ y ∈ t
        exact yt
    . -- ⊢ f x = y
      exact fxy
  . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t
    rintro ⟨x, ⟨xs, xt⟩, fxy⟩
    -- x : α
    -- fxy : f x = y
    -- xs : x ∈ s
    -- xt : x ∈ f ⁻¹' t
    -- ⊢ y ∈ f '' s ∩ t
    constructor
    . -- ⊢ y ∈ f '' s
      use x, xs
      -- ⊢ f x = y
      exact fxy
    . -- ⊢ y ∈ t
      rw [←fxy]
      -- ⊢ f x ∈ t
      rw [←mem_preimage]
      -- ⊢ x ∈ f ⁻¹' t
      exact xt

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by
  ext y
  -- y : β
  -- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
  constructor
  . -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)
    rintro ⟨⟨x, xs, fxy⟩, yt⟩
    -- yt : y ∈ t
    -- x : α
    -- xs : x ∈ s
    -- fxy : f x = y
    -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)
    aesop
  . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t
    rintro ⟨x, ⟨xs, xt⟩, fxy⟩
    -- x : α
    -- fxy : f x = y
    -- xs : x ∈ s
    -- xt : x ∈ f ⁻¹' t
    -- ⊢ y ∈ f '' s ∩ t
    aesop

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by ext ; constructor <;> aesop

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

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
(image_inter_preimage f s t).symm

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

-- variable (x : α)
-- variable (v : Set α)
-- #check (image_inter_preimage f s t : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t)
-- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s)
-- #check (mem_inter : x ∈ s → x ∈ v → x ∈ s ∩ v)
-- #check (mem_preimage : x ∈ f ⁻¹' t ↔ f x ∈ 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

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s : Set α)

variable (t : Set β)

-- 1ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

have h1 : y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t) := by

intro hy

-- hy : y ∈ f '' s ∩ t

-- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)

have h1a : y ∈ f '' s := hy.1

obtain ⟨x : α, hx: x ∈ s ∧ f x = y⟩ := h1a

have h1b : x ∈ s := hx.1

have h1c : f x = y := hx.2

have h1d : y ∈ t := hy.2

have h1e : f x ∈ t := by rwa [←h1c] at h1d

have h1f : x ∈ s ∩ f ⁻¹' t := mem_inter h1b h1e

have h1g : f x ∈ f '' (s ∩ f ⁻¹' t) := mem_image_of_mem f h1f

show y ∈ f '' (s ∩ f ⁻¹' t)

rwa [h1c] at h1g

have h2 : y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t := by

intro hy

-- hy : y ∈ f '' (s ∩ f ⁻¹' t)

-- ⊢ y ∈ f '' s ∩ t

obtain ⟨x : α, hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y⟩ := hy

have h2a : x ∈ s := hx.1.1

have h2b : f x ∈ f '' s := mem_image_of_mem f h2a

have h2c : y ∈ f '' s := by rwa [hx.2] at h2b

have h2d : x ∈ f ⁻¹' t := hx.1.2

have h2e : f x ∈ t := mem_preimage.mp h2d

have h2f : y ∈ t := by rwa [hx.2] at h2e

show y ∈ f '' s ∩ t

exact mem_inter h2c h2f

show y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

exact ⟨h1, h2⟩

-- 2ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

constructor

. -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)

intro hy

-- hy : y ∈ f '' s ∩ t

-- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)

cases' hy with hyfs yt

-- hyfs : y ∈ f '' s

-- yt : y ∈ t

cases' hyfs with x hx

-- x : α

-- hx : x ∈ s ∧ f x = y

cases' hx with xs fxy

-- xs : x ∈ s

-- fxy : f x = y

use x

-- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y

constructor

. -- ⊢ x ∈ s ∩ f ⁻¹' t

constructor

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ f ⁻¹' t

rw [mem_preimage]

-- ⊢ f x ∈ t

rw [fxy]

-- ⊢ y ∈ t

exact yt

. -- ⊢ f x = y

exact fxy

. -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t

intro hy

-- hy : y ∈ f '' (s ∩ f ⁻¹' t)

-- ⊢ y ∈ f '' s ∩ t

cases' hy with x hx

-- x : α

-- hx : x ∈ s ∩ f ⁻¹' t ∧ f x = y

constructor

. -- ⊢ y ∈ f '' s

use x

-- ⊢ x ∈ s ∧ f x = y

constructor

. -- ⊢ x ∈ s

exact hx.1.1

. -- ⊢ f x = y

exact hx.2

. -- ⊢ y ∈ t

cases' hx with hx1 fxy

-- hx1 : x ∈ s ∩ f ⁻¹' t

-- fxy : f x = y

rw [←fxy]

-- ⊢ f x ∈ t

rw [←mem_preimage]

-- ⊢ x ∈ f ⁻¹' t

exact hx1.2

-- 3ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

constructor

. -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)

rintro ⟨⟨x, xs, fxy⟩, yt⟩

-- yt : y ∈ t

-- x : α

-- xs : x ∈ s

-- fxy : f x = y

-- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)

use x

-- ⊢ x ∈ s ∩ f ⁻¹' t ∧ f x = y

constructor

. -- ⊢ x ∈ s ∩ f ⁻¹' t

constructor

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ f ⁻¹' t

rw [mem_preimage]

-- ⊢ f x ∈ t

rw [fxy]

-- ⊢ y ∈ t

exact yt

. -- ⊢ f x = y

exact fxy

. -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t

rintro ⟨x, ⟨xs, xt⟩, fxy⟩

-- x : α

-- fxy : f x = y

-- xs : x ∈ s

-- xt : x ∈ f ⁻¹' t

-- ⊢ y ∈ f '' s ∩ t

constructor

. -- ⊢ y ∈ f '' s

use x, xs

-- ⊢ f x = y

exact fxy

. -- ⊢ y ∈ t

rw [←fxy]

-- ⊢ f x ∈ t

rw [←mem_preimage]

-- ⊢ x ∈ f ⁻¹' t

exact xt

-- 4ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

constructor

. -- ⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)

rintro ⟨⟨x, xs, fxy⟩, yt⟩

-- yt : y ∈ t

-- x : α

-- xs : x ∈ s

-- fxy : f x = y

-- ⊢ y ∈ f '' (s ∩ f ⁻¹' t)

aesop

. -- ⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t

rintro ⟨x, ⟨xs, xt⟩, fxy⟩

-- x : α

-- fxy : f x = y

-- xs : x ∈ s

-- xt : x ∈ f ⁻¹' t

-- ⊢ y ∈ f '' s ∩ t

aesop

-- 5ª demostración

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

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

by ext ; constructor <;> aesop

-- 6ª demostración

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

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

(image_inter_preimage f s t).symm

-- Lemas usados

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

-- variable (x : α)

-- variable (v : Set α)

-- #check (image_inter_preimage f s t : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t)

-- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s)

-- #check (mem_inter : x ∈ s → x ∈ v → x ∈ s ∩ v)

-- #check (mem_preimage : x ∈ f ⁻¹' t ↔ f x ∈ t)

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

3. Demostraciones con Isabelle/HOL

theory Interseccion_con_la_imagen
imports Main
begin

(* 1ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof (rule equalityI)
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof (rule subsetI)
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof (rule IntE)
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof (rule imageE)
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then have "f x ∈ v"
          using ‹y ∈ v› by (rule subst)
        then have "x ∈ f -` v"
          by (rule vimageI2)
        with ‹x ∈ s› have "x ∈ s ∩ f -` v"
          by (rule IntI)
        then have "f x ∈ f ` (s ∩ f -` v)"
          by (rule imageI)
        with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)"
          by (rule ssubst)
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      have "y ∈ f ` s"
      proof -
        have "x ∈ s"
          using hx by (rule IntD1)
        then have "f x ∈ f ` s"
          by (rule imageI)
        with ‹y = f x› show "y ∈ f ` s"
          by (rule ssubst)
      qed
      moreover
      have "y ∈ v"
      proof -
        have "x ∈ f -` v"
          using hx by (rule IntD2)
        then have "f x ∈ v"
          by (rule vimageD)
        with ‹y = f x› show "y ∈ v"
          by (rule ssubst)
      qed
      ultimately show "y ∈ (f ` s) ∩ v"
        by (rule IntI)
    qed
  qed
qed

(* 2ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then have "f x ∈ v" using ‹y ∈ v› by simp
        then have "x ∈ f -` v" by simp
        with ‹x ∈ s› have "x ∈ s ∩ f -` v" by simp
        then have "f x ∈ f ` (s ∩ f -` v)" by simp
        with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      have "y ∈ f ` s"
      proof -
        have "x ∈ s" using hx by simp
        then have "f x ∈ f ` s" by simp
        with ‹y = f x› show "y ∈ f ` s" by simp
      qed
      moreover
      have "y ∈ v"
      proof -
        have "x ∈ f -` v" using hx by simp
        then have "f x ∈ v" by simp
        with ‹y = f x› show "y ∈ v" by simp
      qed
      ultimately show "y ∈ (f ` s) ∩ v" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
proof
  show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)"
  proof
    fix y
    assume "y ∈ (f ` s) ∩ v"
    then show "y ∈ f ` (s ∩ f -` v)"
    proof
      assume "y ∈ v"
      assume "y ∈ f ` s"
      then show "y ∈ f ` (s ∩ f -` v)"
      proof
        fix x
        assume "x ∈ s"
        assume "y = f x"
        then show "y ∈ f ` (s ∩ f -` v)"
          using ‹x ∈ s› ‹y ∈ v› by simp
      qed
    qed
  qed
next
  show "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 hx : "x ∈ s ∩ f -` v"
      then have "y ∈ f ` s" using ‹y = f x› by simp
      moreover
      have "y ∈ v" using hx ‹y = f x› by simp
      ultimately show "y ∈ (f ` s) ∩ v" by simp
    qed
  qed
qed

(* 4ª demostración *)

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
  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

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

theory Interseccion_con_la_imagen

imports Main

begin

(* 1ª demostración *)

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

proof (rule equalityI)

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

proof (rule subsetI)

fix y

assume "y ∈ (f ` s) ∩ v"

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

proof (rule IntE)

assume "y ∈ v"

assume "y ∈ f ` s"

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

proof (rule imageE)

fix x

assume "x ∈ s"

assume "y = f x"

then have "f x ∈ v"

using ‹y ∈ v› by (rule subst)

then have "x ∈ f -` v"

by (rule vimageI2)

with ‹x ∈ s› have "x ∈ s ∩ f -` v"

by (rule IntI)

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

by (rule imageI)

with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)"

by (rule ssubst)

qed

show "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 hx : "x ∈ s ∩ f -` v"

have "y ∈ f ` s"

proof -

have "x ∈ s"

using hx by (rule IntD1)

then have "f x ∈ f ` s"

by (rule imageI)

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

by (rule ssubst)

qed

moreover

have "y ∈ v"

proof -

have "x ∈ f -` v"

using hx by (rule IntD2)

then have "f x ∈ v"

by (rule vimageD)

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

by (rule ssubst)

qed

ultimately show "y ∈ (f ` s) ∩ v"

by (rule IntI)

qed

(* 2ª demostración *)

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

proof

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

proof

fix y

assume "y ∈ (f ` s) ∩ v"

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

proof

assume "y ∈ v"

assume "y ∈ f ` s"

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

proof

fix x

assume "x ∈ s"

assume "y = f x"

then have "f x ∈ v" using ‹y ∈ v› by simp

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

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

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

with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp

qed

show "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 hx : "x ∈ s ∩ f -` v"

have "y ∈ f ` s"

proof -

have "x ∈ s" using hx by simp

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

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

qed

moreover

have "y ∈ v"

proof -

have "x ∈ f -` v" using hx by simp

then have "f x ∈ v" by simp

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

qed

ultimately show "y ∈ (f ` s) ∩ v" by simp

qed

(* 3ª demostración *)

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

proof

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

proof

fix y

assume "y ∈ (f ` s) ∩ v"

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

proof

assume "y ∈ v"

assume "y ∈ f ` s"

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

proof

fix x

assume "x ∈ s"

assume "y = f x"

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

using ‹x ∈ s› ‹y ∈ v› by simp

qed

show "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 hx : "x ∈ s ∩ f -` v"

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

moreover

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

ultimately show "y ∈ (f ` s) ∩ v" by simp

qed

(* 4ª demostración *)

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

by auto

end

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply