f[s ∪ t] = f[s] ∪ f[t]

En Lean4, 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}

1	f '' s = {y \| ∃ x, x ∈ s ∧ f x = y}

Demostrar con Lean4 que

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

1	f '' (s ∪ t) = f '' s ∪ f '' t

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

import Mathlib.Data.Set.Function
variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
open Set

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

import Mathlib.Data.Set.Function

variable {α β : Type _}

variable (f : α → β)

variable (s t : Set α)

open Set

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

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar, para todo \(y\), que
\[ y ∈ f[s ∪ t] ↔ y ∈ f[s] ∪ f[t] \]
Lo haremos mediante la siguiente cadena de equivalencias
\begin{align}
y ∈ f[s ∪ t] &↔ (∃x)(x ∈ s ∪ t ∧ f x = y) \\
&↔ (∃x)((x ∈ s ∨ x ∈ t) ∧ f x = y) \\
&↔ (∃x)((x ∈ s ∧ f x = y) ∨ (x ∈ t ∧ f x = y)) \\
&↔ (∃x)(x ∈ s ∧ f x = y) ∨ (∃x)(x ∈ t ∧ f x = y) \\
&↔ y ∈ f[s] ∨ y ∈ f[t] \\
&↔ y ∈ f[s] ∪ f[t]
\end{align}

2. Demostraciones con Lean4

import Mathlib.Data.Set.Function

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

open 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
  calc y ∈ f '' (s ∪ t)
     ↔ ∃ x, x ∈ s ∪ t ∧ f x = y :=
         by simp only [mem_image]
   _ ↔ ∃ x, (x ∈ s ∨ x ∈ t) ∧ f x = y :=
         by simp only [mem_union]
   _ ↔ ∃ x, (x ∈ s ∧ f x = y) ∨ (x ∈ t ∧ f x = y) :=
         by simp only [or_and_right]
   _ ↔ (∃ x, x ∈ s ∧ f x = y) ∨ (∃ x, x ∈ t ∧ f x = y) :=
         by simp only [exists_or]
   _ ↔ y ∈ f '' s ∨ y ∈ f '' t :=
         by simp only [mem_image]
   _ ↔ y ∈ f '' s ∪ f '' t :=
         by simp only [mem_union]

-- 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 h
    -- h : y ∈ f '' (s ∪ t)
    -- ⊢ y ∈ f '' s ∪ f '' t
    rw [mem_image] at h
    -- h : ∃ x, x ∈ s ∪ t ∧ f x = y
    rcases h with ⟨x, hx⟩
    -- x : α
    -- hx : x ∈ s ∪ t ∧ f x = y
    rcases hx with ⟨xst, fxy⟩
    -- xst : x ∈ s ∪ t
    -- fxy : f x = y
    rw [←fxy]
    -- ⊢ f x ∈ f '' s ∪ f '' t
    rw [mem_union] at xst
    -- xst : x ∈ s ∨ x ∈ t
    rcases xst with (xs | xt)
    . -- xs : x ∈ s
      apply mem_union_left
      -- ⊢ f x ∈ f '' s
      apply mem_image_of_mem
      -- ⊢ x ∈ s
      exact xs
    . -- xt : x ∈ t
      apply mem_union_right
      -- ⊢ f x ∈ f '' t
      apply mem_image_of_mem
      -- ⊢ x ∈ t
      exact xt
  . -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)
    intro h
    -- h : y ∈ f '' s ∪ f '' t
    -- ⊢ y ∈ f '' (s ∪ t)
    rw [mem_union] at h
    -- h : y ∈ f '' s ∨ y ∈ f '' t
    rcases h with (yfs | yft)
    . -- yfs : y ∈ f '' s
      rw [mem_image]
      -- ⊢ ∃ x, x ∈ s ∪ t ∧ f x = y
      rw [mem_image] at yfs
      -- yfs : ∃ x, x ∈ s ∧ f x = y
      rcases yfs with ⟨x, hx⟩
      -- x : α
      -- hx : x ∈ s ∧ f x = y
      rcases hx with ⟨xs, fxy⟩
      -- xs : x ∈ s
      -- fxy : f x = y
      use x
      -- ⊢ x ∈ s ∪ t ∧ f x = y
      constructor
      . -- ⊢ x ∈ s ∪ t
        apply mem_union_left
        -- ⊢ x ∈ s
        exact xs
      . -- ⊢ f x = y
        exact fxy
    . -- yft : y ∈ f '' t
      rw [mem_image]
      -- ⊢ ∃ x, x ∈ s ∪ t ∧ f x = y
      rw [mem_image] at yft
      -- yft : ∃ x, x ∈ t ∧ f x = y
      rcases yft with ⟨x, hx⟩
      -- x : α
      -- hx : x ∈ t ∧ f x = y
      rcases hx with ⟨xt, fxy⟩
      -- xt : x ∈ t
      -- fxy : f x = y
      use x
      -- ⊢ x ∈ s ∪ t ∧ f x = y
      constructor
      . -- ⊢ x ∈ s ∪ t
        apply mem_union_right
        -- ⊢ x ∈ t
        exact xt
      . -- ⊢ f x = y
        exact fxy

-- 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, xst, rfl⟩
    -- x : α
    -- xst : x ∈ s ∪ t
    -- ⊢ f x ∈ f '' s ∪ f '' t
    rcases xst with (xs | xt)
    . -- xs : x ∈ s
      left
      -- ⊢ f x ∈ f '' s
      exact mem_image_of_mem f xs
    . -- xt : x ∈ t
      right
      -- ⊢ f x ∈ f '' t
      exact mem_image_of_mem f xt
  . -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)
    rintro (yfs | yft)
    . -- yfs : y ∈ f '' s
      rcases yfs with ⟨x, xs, rfl⟩
      -- x : α
      -- xs : x ∈ s
      -- ⊢ f x ∈ f '' (s ∪ t)
      apply mem_image_of_mem
      -- ⊢ x ∈ s ∪ t
      left
      -- ⊢ x ∈ s
      exact xs
    . -- yft : y ∈ f '' t
      rcases yft with ⟨x, xt, rfl⟩
      -- x : α
      -- xs : x ∈ s
      -- ⊢ f x ∈ f '' (s ∪ t)
      apply mem_image_of_mem
      -- ⊢ x ∈ s ∪ t
      right
      -- ⊢ x ∈ 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, xst, rfl⟩
    -- x : α
    -- xst : x ∈ s ∪ t
    -- ⊢ f x ∈ f '' s ∪ f '' t
    rcases xst with (xs | xt)
    . -- xs : x ∈ s
      left
      -- ⊢ f x ∈ f '' s
      use x, xs
    . -- xt : x ∈ t
      right
      -- ⊢ f x ∈ f '' t
      use x, xt
  . rintro (yfs | yft)
    . -- yfs : y ∈ f '' s
      rcases yfs with ⟨x, xs, rfl⟩
      -- x : α
      -- xs : x ∈ s
      -- ⊢ f x ∈ f '' (s ∪ t)
      use x, Or.inl xs
    . -- yft : y ∈ f '' t
      rcases yft with ⟨x, xt, rfl⟩
      -- x : α
      -- xt : x ∈ t
      -- ⊢ f x ∈ f '' (s ∪ t)
      use x, Or.inr xt

-- 5ª 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 | xt, rfl⟩
    . -- x : α
      -- xs : x ∈ s
      -- ⊢ f x ∈ f '' s ∪ f '' t
      left
      -- ⊢ f x ∈ f '' s
      use x, xs
    . -- x : α
      -- xt : x ∈ t
      -- ⊢ f x ∈ f '' s ∪ f '' t
      right
      -- ⊢ f x ∈ f '' t
      use x, xt
  . -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)
    rintro (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩)
    . -- x : α
      -- xs : x ∈ s
      -- ⊢ f x ∈ f '' (s ∪ t)
      use x, Or.inl xs
    . -- x : α
      -- xt : x ∈ t
      -- ⊢ f x ∈ f '' (s ∪ t)
      use x, Or.inr xt

-- 6ª 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
    aesop
  . -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)
    aesop

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
by
  ext y
  constructor <;> aesop

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

example : f '' (s ∪ t) = f '' s ∪ f '' t :=
by
  ext y
  -- y : β
  -- ⊢ y ∈ f '' (s ∪ t) ↔ y ∈ f '' s ∪ f '' t
  rw [iff_def]
  -- ⊢ (y ∈ f '' (s ∪ t) → y ∈ f '' s ∪ f '' t) ∧ (y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t))
  aesop

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

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

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

-- variable (x : α)
-- variable (y : β)
-- variable (a b c : Prop)
-- variable (p q : α → Prop)
-- #check (Or.inl : a → a ∨ b)
-- #check (Or.inr : b → a ∨ b)
-- #check (exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x)
-- #check (iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a))
-- #check (image_union f s t : f '' (s ∪ t) = f '' s ∪ f '' t)
-- #check (mem_image f s y : (y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y))
-- #check (mem_image_of_mem  f : x ∈ s → f x ∈ f '' s)
-- #check (mem_union x s t : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t)
-- #check (mem_union_left t : x ∈ s → x ∈ s ∪ t)
-- #check (mem_union_right s : x ∈ t → x ∈ s ∪ t)
-- #check (or_and_right : (a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c)

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

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

import Mathlib.Data.Set.Function

variable {α β : Type _}

variable (f : α → β)

variable (s t : Set α)

open Set

-- 1ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' (s ∪ t) ↔ y ∈ f '' s ∪ f '' t

calc y ∈ f '' (s ∪ t)

↔ ∃ x, x ∈ s ∪ t ∧ f x = y :=

by simp only [mem_image]

_ ↔ ∃ x, (x ∈ s ∨ x ∈ t) ∧ f x = y :=

by simp only [mem_union]

_ ↔ ∃ x, (x ∈ s ∧ f x = y) ∨ (x ∈ t ∧ f x = y) :=

by simp only [or_and_right]

_ ↔ (∃ x, x ∈ s ∧ f x = y) ∨ (∃ x, x ∈ t ∧ f x = y) :=

by simp only [exists_or]

_ ↔ y ∈ f '' s ∨ y ∈ f '' t :=

by simp only [mem_image]

_ ↔ y ∈ f '' s ∪ f '' t :=

by simp only [mem_union]

-- 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 h

-- h : y ∈ f '' (s ∪ t)

-- ⊢ y ∈ f '' s ∪ f '' t

rw [mem_image] at h

-- h : ∃ x, x ∈ s ∪ t ∧ f x = y

rcases h with ⟨x, hx⟩

-- x : α

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

rcases hx with ⟨xst, fxy⟩

-- xst : x ∈ s ∪ t

-- fxy : f x = y

rw [←fxy]

-- ⊢ f x ∈ f '' s ∪ f '' t

rw [mem_union] at xst

-- xst : x ∈ s ∨ x ∈ t

rcases xst with (xs | xt)

. -- xs : x ∈ s

apply mem_union_left

-- ⊢ f x ∈ f '' s

apply mem_image_of_mem

-- ⊢ x ∈ s

exact xs

. -- xt : x ∈ t

apply mem_union_right

-- ⊢ f x ∈ f '' t

apply mem_image_of_mem

-- ⊢ x ∈ t

exact xt

. -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)

intro h

-- h : y ∈ f '' s ∪ f '' t

-- ⊢ y ∈ f '' (s ∪ t)

rw [mem_union] at h

-- h : y ∈ f '' s ∨ y ∈ f '' t

rcases h with (yfs | yft)

. -- yfs : y ∈ f '' s

rw [mem_image]

-- ⊢ ∃ x, x ∈ s ∪ t ∧ f x = y

rw [mem_image] at yfs

-- yfs : ∃ x, x ∈ s ∧ f x = y

rcases yfs with ⟨x, hx⟩

-- x : α

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

rcases hx with ⟨xs, fxy⟩

-- xs : x ∈ s

-- fxy : f x = y

use x

-- ⊢ x ∈ s ∪ t ∧ f x = y

constructor

. -- ⊢ x ∈ s ∪ t

apply mem_union_left

-- ⊢ x ∈ s

exact xs

. -- ⊢ f x = y

exact fxy

. -- yft : y ∈ f '' t

rw [mem_image]

-- ⊢ ∃ x, x ∈ s ∪ t ∧ f x = y

rw [mem_image] at yft

-- yft : ∃ x, x ∈ t ∧ f x = y

rcases yft with ⟨x, hx⟩

-- x : α

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

rcases hx with ⟨xt, fxy⟩

-- xt : x ∈ t

-- fxy : f x = y

use x

-- ⊢ x ∈ s ∪ t ∧ f x = y

constructor

. -- ⊢ x ∈ s ∪ t

apply mem_union_right

-- ⊢ x ∈ t

exact xt

. -- ⊢ f x = y

exact fxy

-- 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, xst, rfl⟩

-- x : α

-- xst : x ∈ s ∪ t

-- ⊢ f x ∈ f '' s ∪ f '' t

rcases xst with (xs | xt)

. -- xs : x ∈ s

left

-- ⊢ f x ∈ f '' s

exact mem_image_of_mem f xs

. -- xt : x ∈ t

right

-- ⊢ f x ∈ f '' t

exact mem_image_of_mem f xt

. -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)

rintro (yfs | yft)

. -- yfs : y ∈ f '' s

rcases yfs with ⟨x, xs, rfl⟩

-- x : α

-- xs : x ∈ s

-- ⊢ f x ∈ f '' (s ∪ t)

apply mem_image_of_mem

-- ⊢ x ∈ s ∪ t

left

-- ⊢ x ∈ s

exact xs

. -- yft : y ∈ f '' t

rcases yft with ⟨x, xt, rfl⟩

-- x : α

-- xs : x ∈ s

-- ⊢ f x ∈ f '' (s ∪ t)

apply mem_image_of_mem

-- ⊢ x ∈ s ∪ t

right

-- ⊢ x ∈ 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, xst, rfl⟩

-- x : α

-- xst : x ∈ s ∪ t

-- ⊢ f x ∈ f '' s ∪ f '' t

rcases xst with (xs | xt)

. -- xs : x ∈ s

left

-- ⊢ f x ∈ f '' s

use x, xs

. -- xt : x ∈ t

right

-- ⊢ f x ∈ f '' t

use x, xt

. rintro (yfs | yft)

. -- yfs : y ∈ f '' s

rcases yfs with ⟨x, xs, rfl⟩

-- x : α

-- xs : x ∈ s

-- ⊢ f x ∈ f '' (s ∪ t)

use x, Or.inl xs

. -- yft : y ∈ f '' t

rcases yft with ⟨x, xt, rfl⟩

-- x : α

-- xt : x ∈ t

-- ⊢ f x ∈ f '' (s ∪ t)

use x, Or.inr xt

-- 5ª 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 | xt, rfl⟩

. -- x : α

-- xs : x ∈ s

-- ⊢ f x ∈ f '' s ∪ f '' t

left

-- ⊢ f x ∈ f '' s

use x, xs

. -- x : α

-- xt : x ∈ t

-- ⊢ f x ∈ f '' s ∪ f '' t

right

-- ⊢ f x ∈ f '' t

use x, xt

. -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)

rintro (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩)

. -- x : α

-- xs : x ∈ s

-- ⊢ f x ∈ f '' (s ∪ t)

use x, Or.inl xs

. -- x : α

-- xt : x ∈ t

-- ⊢ f x ∈ f '' (s ∪ t)

use x, Or.inr xt

-- 6ª 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

aesop

. -- ⊢ y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t)

aesop

-- 7ª demostración

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

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

ext y

constructor <;> aesop

-- 8ª demostración

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

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

ext y

-- y : β

-- ⊢ y ∈ f '' (s ∪ t) ↔ y ∈ f '' s ∪ f '' t

rw [iff_def]

-- ⊢ (y ∈ f '' (s ∪ t) → y ∈ f '' s ∪ f '' t) ∧ (y ∈ f '' s ∪ f '' t → y ∈ f '' (s ∪ t))

aesop

-- 9ª demostración

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

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

image_union f s t

-- Lemas usados

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

-- variable (x : α)

-- variable (y : β)

-- variable (a b c : Prop)

-- variable (p q : α → Prop)

-- #check (Or.inl : a → a ∨ b)

-- #check (Or.inr : b → a ∨ b)

-- #check (exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x)

-- #check (iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a))

-- #check (image_union f s t : f '' (s ∪ t) = f '' s ∪ f '' t)

-- #check (mem_image f s y : (y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y))

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

-- #check (mem_union x s t : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t)

-- #check (mem_union_left t : x ∈ s → x ∈ s ∪ t)

-- #check (mem_union_right s : x ∈ t → x ∈ s ∪ t)

-- #check (or_and_right : (a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c)

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

3. Demostraciones con Isabelle/HOL

theory Imagen_de_la_union
imports Main
begin

(* 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

(* 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

(* 3ª demostración *)
lemma "f ` (s ∪ t) = f ` s ∪ f ` t"
  by (simp only: image_Un)

(* 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

theory Imagen_de_la_union

imports Main

begin

(* 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

(* 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

(* 3ª demostración *)

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

by (simp only: image_Un)

(* 4ª demostración *)

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

by auto

end

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply