Diferencia de unión e intersección

Demostrar que

(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)

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

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

sorry

Soluciones

Soluciones con Lean

import data.set.basic
open set

variable {α : Type}
variables s t : set α

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
begin
  ext x,
  split,
  { rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩),
    { split,
      { left,
        exact xs },
      { rintros ⟨_, xt⟩,
        contradiction }},
    { split ,
      { right,
        exact xt },
      { rintros ⟨xs, _⟩,
        contradiction }}},
  { rintros ⟨xs | xt, nxst⟩,
    { left,
      use xs,
      intro xt,
      apply nxst,
      split; assumption },
    { right,
      use xt,
      intro xs,
      apply nxst,
      split; assumption }},
end

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
begin
  ext x,
  split,
  { rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩),
    { finish, },
    { finish, }},
  { rintros ⟨xs | xt, nxst⟩,
    { finish, },
    { finish, }},
end

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
begin
  ext x,
  split,
  { rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩) ; finish, },
  { rintros ⟨xs | xt, nxst⟩ ; finish, },
end

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
begin
  ext,
  split,
  { finish, },
  { finish, },
end

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
begin
  rw ext_iff,
  intro,
  rw iff_def,
  finish,
end

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by finish [ext_iff, iff_def]

import data.set.basic

open set

variable {α : Type}

variables s t : set α

-- 1ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

begin

ext x,

split,

{ rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩),

{ split,

{ left,

exact xs },

{ rintros ⟨_, xt⟩,

contradiction }},

{ split ,

{ right,

exact xt },

{ rintros ⟨xs, _⟩,

contradiction }}},

{ rintros ⟨xs | xt, nxst⟩,

{ left,

use xs,

intro xt,

apply nxst,

split; assumption },

{ right,

use xt,

intro xs,

apply nxst,

split; assumption }},

end

-- 2ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

begin

ext x,

split,

{ rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩),

{ finish, },

{ finish, }},

{ rintros ⟨xs | xt, nxst⟩,

{ finish, },

{ finish, }},

end

-- 3ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

begin

ext x,

split,

{ rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩) ; finish, },

{ rintros ⟨xs | xt, nxst⟩ ; finish, },

end

-- 4ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

begin

ext,

split,

{ finish, },

end

-- 5ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

begin

rw ext_iff,

intro,

rw iff_def,

finish,

end

-- 6ª demostración

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

by finish [ext_iff, iff_def]

Soluciones con Isabelle/HOL

theory Diferencia_de_union_e_interseccion
imports Main
begin

section ‹1 demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
proof (rule equalityI)
  show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (s - t) ∪ (t - s)"
    then show "x ∈ (s ∪ t) - (s ∩ t)"
    proof (rule UnE)
      assume "x ∈ s - t"
      then show "x ∈ (s ∪ t) - (s ∩ t)"
      proof (rule DiffE)
        assume "x ∈ s"
        assume "x ∉ t"
        have "x ∈ s ∪ t"
          using ‹x ∈ s› by (simp only: UnI1)
        moreover
        have "x ∉ s ∩ t"
        proof (rule notI)
          assume "x ∈ s ∩ t"
          then have "x ∈ t"
            by (simp only: IntD2)
          with ‹x ∉ t› show False
            by (rule notE)
        qed
        ultimately show "x ∈ (s ∪ t) - (s ∩ t)"
          by (rule DiffI)
      qed
    next
      assume "x ∈ t - s"
      then show "x ∈ (s ∪ t) - (s ∩ t)"
      proof (rule DiffE)
        assume "x ∈ t"
        assume "x ∉ s"
        have "x ∈ s ∪ t"
          using ‹x ∈ t› by (simp only: UnI2)
        moreover
        have "x ∉ s ∩ t"
        proof (rule notI)
          assume "x ∈ s ∩ t"
          then have "x ∈ s"
            by (simp only: IntD1)
          with ‹x ∉ s› show False
            by (rule notE)
        qed
        ultimately show "x ∈ (s ∪ t) - (s ∩ t)"
          by (rule DiffI)
      qed
    qed
  qed
next
  show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (s ∪ t) - (s ∩ t)"
    then show "x ∈ (s - t) ∪ (t - s)"
    proof (rule DiffE)
      assume "x ∈ s ∪ t"
      assume "x ∉ s ∩ t"
      note ‹x ∈ s ∪ t›
      then show "x ∈ (s - t) ∪ (t - s)"
      proof (rule UnE)
        assume "x ∈ s"
        have "x ∉ t"
        proof (rule notI)
          assume "x ∈ t"
          with ‹x ∈ s› have "x ∈ s ∩ t"
            by (rule IntI)
          with ‹x ∉ s ∩ t› show False
            by (rule notE)
        qed
        with ‹x ∈ s› have "x ∈ s - t"
          by (rule DiffI)
        then show "x ∈ (s - t) ∪ (t - s)"
          by (simp only: UnI1)
      next
        assume "x ∈ t"
        have "x ∉ s"
        proof (rule notI)
          assume "x ∈ s"
          then have "x ∈ s ∩ t"
            using ‹x ∈ t› by (rule IntI)
          with ‹x ∉ s ∩ t› show False
            by (rule notE)
        qed
        with ‹x ∈ t› have "x ∈ t - s"
          by (rule DiffI)
        then show "x ∈ (s - t) ∪ (t - s)"
          by (rule UnI2)
      qed
    qed
  qed
qed

section ‹2 demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
proof
  show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"
  proof
    fix x
    assume "x ∈ (s - t) ∪ (t - s)"
    then show "x ∈ (s ∪ t) - (s ∩ t)"
    proof
      assume "x ∈ s - t"
      then show "x ∈ (s ∪ t) - (s ∩ t)"
      proof
        assume "x ∈ s"
        assume "x ∉ t"
        have "x ∈ s ∪ t"
          using ‹x ∈ s› by simp
        moreover
        have "x ∉ s ∩ t"
        proof
          assume "x ∈ s ∩ t"
          then have "x ∈ t"
            by simp
          with ‹x ∉ t› show False
            by simp
        qed
        ultimately show "x ∈ (s ∪ t) - (s ∩ t)"
          by simp
      qed
    next
      assume "x ∈ t - s"
      then show "x ∈ (s ∪ t) - (s ∩ t)"
      proof
        assume "x ∈ t"
        assume "x ∉ s"
        have "x ∈ s ∪ t"
          using ‹x ∈ t› by simp
        moreover
        have "x ∉ s ∩ t"
        proof
          assume "x ∈ s ∩ t"
          then have "x ∈ s"
            by simp
          with ‹x ∉ s› show False
            by simp
        qed
        ultimately show "x ∈ (s ∪ t) - (s ∩ t)"
          by simp
      qed
    qed
  qed
next
  show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"
  proof
    fix x
    assume "x ∈ (s ∪ t) - (s ∩ t)"
    then show "x ∈ (s - t) ∪ (t - s)"
    proof
      assume "x ∈ s ∪ t"
      assume "x ∉ s ∩ t"
      note ‹x ∈ s ∪ t›
      then show "x ∈ (s - t) ∪ (t - s)"
      proof
        assume "x ∈ s"
        have "x ∉ t"
        proof
          assume "x ∈ t"
          with ‹x ∈ s› have "x ∈ s ∩ t"
            by simp
          with ‹x ∉ s ∩ t› show False
            by simp
        qed
        with ‹x ∈ s› have "x ∈ s - t"
          by simp
        then show "x ∈ (s - t) ∪ (t - s)"
          by simp
      next
        assume "x ∈ t"
        have "x ∉ s"
        proof
          assume "x ∈ s"
          then have "x ∈ s ∩ t"
            using ‹x ∈ t› by simp
          with ‹x ∉ s ∩ t› show False
            by simp
        qed
        with ‹x ∈ t› have "x ∈ t - s"
          by simp
        then show "x ∈ (s - t) ∪ (t - s)"
          by simp
      qed
    qed
  qed
qed

section ‹3ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
proof
  show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"
  proof
    fix x
    assume "x ∈ (s - t) ∪ (t - s)"
    then show "x ∈ (s ∪ t) - (s ∩ t)"
    proof
      assume "x ∈ s - t"
      then show "x ∈ (s ∪ t) - (s ∩ t)" by simp
    next
      assume "x ∈ t - s"
      then show "x ∈ (s ∪ t) - (s ∩ t)" by simp
    qed
  qed
next
  show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"
  proof
    fix x
    assume "x ∈ (s ∪ t) - (s ∩ t)"
    then show "x ∈ (s - t) ∪ (t - s)"
    proof
      assume "x ∈ s ∪ t"
      assume "x ∉ s ∩ t"
      note ‹x ∈ s ∪ t›
      then show "x ∈ (s - t) ∪ (t - s)"
      proof
        assume "x ∈ s"
        then show "x ∈ (s - t) ∪ (t - s)"
          using ‹x ∉ s ∩ t› by simp
      next
        assume "x ∈ t"
        then show "x ∈ (s - t) ∪ (t - s)"
          using ‹x ∉ s ∩ t› by simp
      qed
    qed
  qed
qed

section ‹4ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
proof
  show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"
  proof
    fix x
    assume "x ∈ (s - t) ∪ (t - s)"
    then show "x ∈ (s ∪ t) - (s ∩ t)" by auto
  qed
next
  show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"
  proof
    fix x
    assume "x ∈ (s ∪ t) - (s ∩ t)"
    then show "x ∈ (s - t) ∪ (t - s)" by auto
  qed
qed

section ‹5ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"
proof
  show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)" by auto
next
  show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)" by auto
qed

section ‹6ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ 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

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

theory Diferencia_de_union_e_interseccion

imports Main

begin

section ‹1 demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

proof (rule equalityI)

show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"

proof (rule subsetI)

fix x

assume "x ∈ (s - t) ∪ (t - s)"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof (rule UnE)

assume "x ∈ s - t"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof (rule DiffE)

assume "x ∈ s"

assume "x ∉ t"

have "x ∈ s ∪ t"

using ‹x ∈ s› by (simp only: UnI1)

moreover

have "x ∉ s ∩ t"

proof (rule notI)

assume "x ∈ s ∩ t"

then have "x ∈ t"

by (simp only: IntD2)

with ‹x ∉ t› show False

by (rule notE)

qed

ultimately show "x ∈ (s ∪ t) - (s ∩ t)"

by (rule DiffI)

qed

assume "x ∈ t - s"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof (rule DiffE)

assume "x ∈ t"

assume "x ∉ s"

have "x ∈ s ∪ t"

using ‹x ∈ t› by (simp only: UnI2)

moreover

have "x ∉ s ∩ t"

proof (rule notI)

assume "x ∈ s ∩ t"

then have "x ∈ s"

by (simp only: IntD1)

with ‹x ∉ s› show False

by (rule notE)

qed

ultimately show "x ∈ (s ∪ t) - (s ∩ t)"

by (rule DiffI)

qed

show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"

proof (rule subsetI)

fix x

assume "x ∈ (s ∪ t) - (s ∩ t)"

then show "x ∈ (s - t) ∪ (t - s)"

proof (rule DiffE)

assume "x ∈ s ∪ t"

assume "x ∉ s ∩ t"

note ‹x ∈ s ∪ t›

then show "x ∈ (s - t) ∪ (t - s)"

proof (rule UnE)

assume "x ∈ s"

have "x ∉ t"

proof (rule notI)

assume "x ∈ t"

with ‹x ∈ s› have "x ∈ s ∩ t"

by (rule IntI)

with ‹x ∉ s ∩ t› show False

by (rule notE)

qed

with ‹x ∈ s› have "x ∈ s - t"

by (rule DiffI)

then show "x ∈ (s - t) ∪ (t - s)"

by (simp only: UnI1)

assume "x ∈ t"

have "x ∉ s"

proof (rule notI)

assume "x ∈ s"

then have "x ∈ s ∩ t"

using ‹x ∈ t› by (rule IntI)

with ‹x ∉ s ∩ t› show False

by (rule notE)

qed

with ‹x ∈ t› have "x ∈ t - s"

by (rule DiffI)

then show "x ∈ (s - t) ∪ (t - s)"

by (rule UnI2)

qed

section ‹2 demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

proof

show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"

proof

fix x

assume "x ∈ (s - t) ∪ (t - s)"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof

assume "x ∈ s - t"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof

assume "x ∈ s"

assume "x ∉ t"

have "x ∈ s ∪ t"

using ‹x ∈ s› by simp

moreover

have "x ∉ s ∩ t"

proof

assume "x ∈ s ∩ t"

then have "x ∈ t"

by simp

with ‹x ∉ t› show False

by simp

qed

ultimately show "x ∈ (s ∪ t) - (s ∩ t)"

by simp

qed

assume "x ∈ t - s"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof

assume "x ∈ t"

assume "x ∉ s"

have "x ∈ s ∪ t"

using ‹x ∈ t› by simp

moreover

have "x ∉ s ∩ t"

proof

assume "x ∈ s ∩ t"

then have "x ∈ s"

by simp

with ‹x ∉ s› show False

by simp

qed

ultimately show "x ∈ (s ∪ t) - (s ∩ t)"

by simp

qed

show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"

proof

fix x

assume "x ∈ (s ∪ t) - (s ∩ t)"

then show "x ∈ (s - t) ∪ (t - s)"

proof

assume "x ∈ s ∪ t"

assume "x ∉ s ∩ t"

note ‹x ∈ s ∪ t›

then show "x ∈ (s - t) ∪ (t - s)"

proof

assume "x ∈ s"

have "x ∉ t"

proof

assume "x ∈ t"

with ‹x ∈ s› have "x ∈ s ∩ t"

by simp

with ‹x ∉ s ∩ t› show False

by simp

qed

with ‹x ∈ s› have "x ∈ s - t"

by simp

then show "x ∈ (s - t) ∪ (t - s)"

by simp

assume "x ∈ t"

have "x ∉ s"

proof

assume "x ∈ s"

then have "x ∈ s ∩ t"

using ‹x ∈ t› by simp

with ‹x ∉ s ∩ t› show False

by simp

qed

with ‹x ∈ t› have "x ∈ t - s"

by simp

then show "x ∈ (s - t) ∪ (t - s)"

by simp

qed

section ‹3ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

proof

show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"

proof

fix x

assume "x ∈ (s - t) ∪ (t - s)"

then show "x ∈ (s ∪ t) - (s ∩ t)"

proof

assume "x ∈ s - t"

then show "x ∈ (s ∪ t) - (s ∩ t)" by simp

assume "x ∈ t - s"

then show "x ∈ (s ∪ t) - (s ∩ t)" by simp

qed

show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"

proof

fix x

assume "x ∈ (s ∪ t) - (s ∩ t)"

then show "x ∈ (s - t) ∪ (t - s)"

proof

assume "x ∈ s ∪ t"

assume "x ∉ s ∩ t"

note ‹x ∈ s ∪ t›

then show "x ∈ (s - t) ∪ (t - s)"

proof

assume "x ∈ s"

then show "x ∈ (s - t) ∪ (t - s)"

using ‹x ∉ s ∩ t› by simp

assume "x ∈ t"

then show "x ∈ (s - t) ∪ (t - s)"

using ‹x ∉ s ∩ t› by simp

qed

section ‹4ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

proof

show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)"

proof

fix x

assume "x ∈ (s - t) ∪ (t - s)"

then show "x ∈ (s ∪ t) - (s ∩ t)" by auto

qed

show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)"

proof

fix x

assume "x ∈ (s ∪ t) - (s ∩ t)"

then show "x ∈ (s - t) ∪ (t - s)" by auto

qed

section ‹5ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

proof

show "(s - t) ∪ (t - s) ⊆ (s ∪ t) - (s ∩ t)" by auto

show "(s ∪ t) - (s ∩ t) ⊆ (s - t) ∪ (t - s)" by auto

qed

section ‹6ª demostración›

lemma "(s - t) ∪ (t - s) = (s ∪ t) - (s ∩ t)"

by auto

end

Nuevas soluciones

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

Soluciones

Share this:

Escribe un comentarioCancel reply