Unión con intersección general

Demostrar que

   s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)

1	s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)

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

import data.set.basic
import tactic

open set

variable  {α : Type}
variable  s : set α
variables A : ℕ → set α

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
sorry

import data.set.basic

import tactic

open set

variable {α : Type}

variable s : set α

variables A : ℕ → set α

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

sorry

Soluciones

Soluciones con Lean

import data.set.basic
import tactic

open set

variable  {α : Type}
variable  s : set α
variables A : ℕ → set α

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext x,
  simp only [mem_union, mem_Inter],
  split,
  { intros h i,
    cases h with xs xAi,
    { right,
      exact xs },
    { left,
      exact xAi i, }},
  { intro h,
    by_cases xs : x ∈ s,
    { left,
      exact xs },
    { right,
      intro i,
      cases h i with xAi xs,
      { exact xAi, },
      { contradiction, }}},
end

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext x,
  simp only [mem_union, mem_Inter],
  split,
  { rintros (xs | xI) i,
    { right,
      exact xs },
    { left,
      exact xI i }},
  { intro h,
    by_cases xs : x ∈ s,
    { left,
      exact xs },
    { right,
      intro i,
      cases h i,
      { assumption },
      { contradiction }}},
end

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext x,
  simp only [mem_union, mem_Inter],
  split,
  { finish, },
  { finish, },
end

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext,
  simp only [mem_union, mem_Inter],
  split ; finish,
end

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext,
  simp only [mem_union, mem_Inter],
  finish [iff_def],
end

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
by finish [ext_iff, mem_union, mem_Inter, iff_def]

import data.set.basic

import tactic

open set

variable {α : Type}

variable s : set α

variables A : ℕ → set α

-- 1ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

begin

ext x,

simp only [mem_union, mem_Inter],

split,

{ intros h i,

cases h with xs xAi,

{ right,

exact xs },

{ left,

exact xAi i, }},

{ intro h,

by_cases xs : x ∈ s,

{ left,

exact xs },

{ right,

intro i,

cases h i with xAi xs,

{ exact xAi, },

{ contradiction, }}},

end

-- 2ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

begin

ext x,

simp only [mem_union, mem_Inter],

split,

{ rintros (xs | xI) i,

{ right,

exact xs },

{ left,

exact xI i }},

{ intro h,

by_cases xs : x ∈ s,

{ left,

exact xs },

{ right,

intro i,

cases h i,

{ assumption },

{ contradiction }}},

end

-- 3ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

begin

ext x,

simp only [mem_union, mem_Inter],

split,

{ finish, },

end

-- 4ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

begin

ext,

simp only [mem_union, mem_Inter],

split ; finish,

end

-- 5ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

begin

ext,

simp only [mem_union, mem_Inter],

finish [iff_def],

end

-- 6ª demostración

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

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

by finish [ext_iff, mem_union, mem_Inter, iff_def]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Soluciones con Isabelle/HOL

theory Union_con_interseccion_general
imports Main
begin

section ‹1ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
proof (rule equalityI)
  show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" 
  proof (rule subsetI)
    fix x
    assume "x ∈ s ∪ (⋂ i ∈ I. A i)"
    then show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
    proof (rule UnE)
      assume "x ∈ s"
      show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
      proof (rule INT_I)
        fix i
        assume "i ∈ I"
        show "x ∈ A i ∪ s" 
          using ‹x ∈ s› by (rule UnI2)
      qed 
    next
      assume h1 : "x ∈ (⋂ i ∈ I. A i)"
      show "x ∈ (⋂ i ∈ I. A i ∪ s)"
      proof (rule INT_I)
        fix i
        assume "i ∈ I"
        with h1 have "x ∈ A i" 
          by (rule INT_D)
        then show "x ∈ A i ∪ s" 
          by (rule UnI1)
      qed 
    qed
  qed
next
  show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" 
  proof (rule subsetI)
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"
    show "x ∈ s ∪ (⋂ i ∈ I. A i)"
    proof (cases "x ∈ s")
      assume "x ∈ s"
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        by (rule UnI1)
    next
      assume "x ∉ s"
      have "x ∈ (⋂ i ∈ I. A i)" 
      proof (rule INT_I)
        fix i
        assume "i ∈ I"
        with h2 have "x ∈ A i ∪ s" 
          by (rule INT_D)
        then show "x ∈ A i"
        proof (rule UnE)
          assume "x ∈ A i"
          then show "x ∈ A i"
            by this
        next
          assume "x ∈ s"
          with ‹x ∉ s› show "x ∈ A i" 
            by (rule notE)
        qed
      qed 
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        by (rule UnI2)
    qed
  qed
qed

section ‹2ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
proof 
  show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" 
  proof 
    fix x
    assume "x ∈ s ∪ (⋂ i ∈ I. A i)"
    then show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
    proof 
      assume "x ∈ s"
      show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
      proof 
        fix i
        assume "i ∈ I"
        show "x ∈ A i ∪ s" 
          using ‹x ∈ s› by simp
      qed 
    next
      assume h1 : "x ∈ (⋂ i ∈ I. A i)"
      show "x ∈ (⋂ i ∈ I. A i ∪ s)"
      proof 
        fix i
        assume "i ∈ I"
        with h1 have "x ∈ A i" 
          by simp
        then show "x ∈ A i ∪ s" 
          by simp
      qed 
    qed
  qed
next
  show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" 
  proof 
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"
    show "x ∈ s ∪ (⋂ i ∈ I. A i)"
    proof (cases "x ∈ s")
      assume "x ∈ s"
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        by simp
    next
      assume "x ∉ s"
      have "x ∈ (⋂ i ∈ I. A i)" 
      proof 
        fix i
        assume "i ∈ I"
        with h2 have "x ∈ A i ∪ s" 
          by (rule INT_D)
        then show "x ∈ A i"
        proof 
          assume "x ∈ A i"
          then show "x ∈ A i"
            by this
        next
          assume "x ∈ s"
          with ‹x ∉ s› show "x ∈ A i" 
            by simp
        qed
      qed 
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        by simp
    qed
  qed
qed

section ‹3ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
proof 
  show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" 
  proof 
    fix x
    assume "x ∈ s ∪ (⋂ i ∈ I. A i)"
    then show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
    proof 
      assume "x ∈ s"
      then show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
        by simp
    next
      assume "x ∈ (⋂ i ∈ I. A i)"
      then show "x ∈ (⋂ i ∈ I. A i ∪ s)"
        by simp
    qed
  qed
next
  show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" 
  proof 
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"
    show "x ∈ s ∪ (⋂ i ∈ I. A i)"
    proof (cases "x ∈ s")
      assume "x ∈ s"
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        by simp
    next
      assume "x ∉ s"
      then show "x ∈ s ∪ (⋂ i ∈ I. A i)" 
        using h2 by simp
    qed
  qed
qed

section ‹4ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
proof 
  show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)" 
  proof 
    fix x
    assume "x ∈ s ∪ (⋂ i ∈ I. A i)"
    then show "x ∈ (⋂ i ∈ I. A i ∪ s)" 
    proof 
      assume "x ∈ s"
      then show ?thesis by simp
    next
      assume "x ∈ (⋂ i ∈ I. A i)"
      then show ?thesis by simp
    qed
  qed
next
  show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)" 
  proof 
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"
    show "x ∈ s ∪ (⋂ i ∈ I. A i)"
    proof (cases "x ∈ s")
      case True
      then show ?thesis by simp
    next
      case False
      then show ?thesis using h2 by simp
    qed
  qed
qed

section ‹5ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"
  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

theory Union_con_interseccion_general

imports Main

begin

section ‹1ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"

proof (rule equalityI)

show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)"

proof (rule subsetI)

fix x

assume "x ∈ s ∪ (⋂ i ∈ I. A i)"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof (rule UnE)

assume "x ∈ s"

show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof (rule INT_I)

fix i

assume "i ∈ I"

show "x ∈ A i ∪ s"

using ‹x ∈ s› by (rule UnI2)

qed

assume h1 : "x ∈ (⋂ i ∈ I. A i)"

show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with h1 have "x ∈ A i"

by (rule INT_D)

then show "x ∈ A i ∪ s"

by (rule UnI1)

qed

show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)"

proof (rule subsetI)

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"

show "x ∈ s ∪ (⋂ i ∈ I. A i)"

proof (cases "x ∈ s")

assume "x ∈ s"

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

by (rule UnI1)

assume "x ∉ s"

have "x ∈ (⋂ i ∈ I. A i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

with h2 have "x ∈ A i ∪ s"

by (rule INT_D)

then show "x ∈ A i"

proof (rule UnE)

assume "x ∈ A i"

then show "x ∈ A i"

by this

assume "x ∈ s"

with ‹x ∉ s› show "x ∈ A i"

by (rule notE)

qed

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

by (rule UnI2)

qed

section ‹2ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"

proof

show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)"

proof

fix x

assume "x ∈ s ∪ (⋂ i ∈ I. A i)"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof

assume "x ∈ s"

show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof

fix i

assume "i ∈ I"

show "x ∈ A i ∪ s"

using ‹x ∈ s› by simp

qed

assume h1 : "x ∈ (⋂ i ∈ I. A i)"

show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof

fix i

assume "i ∈ I"

with h1 have "x ∈ A i"

by simp

then show "x ∈ A i ∪ s"

by simp

qed

show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)"

proof

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"

show "x ∈ s ∪ (⋂ i ∈ I. A i)"

proof (cases "x ∈ s")

assume "x ∈ s"

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

by simp

assume "x ∉ s"

have "x ∈ (⋂ i ∈ I. A i)"

proof

fix i

assume "i ∈ I"

with h2 have "x ∈ A i ∪ s"

by (rule INT_D)

then show "x ∈ A i"

proof

assume "x ∈ A i"

then show "x ∈ A i"

by this

assume "x ∈ s"

with ‹x ∉ s› show "x ∈ A i"

by simp

qed

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

by simp

qed

section ‹3ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"

proof

show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)"

proof

fix x

assume "x ∈ s ∪ (⋂ i ∈ I. A i)"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof

assume "x ∈ s"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

by simp

assume "x ∈ (⋂ i ∈ I. A i)"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

by simp

qed

show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)"

proof

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"

show "x ∈ s ∪ (⋂ i ∈ I. A i)"

proof (cases "x ∈ s")

assume "x ∈ s"

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

by simp

assume "x ∉ s"

then show "x ∈ s ∪ (⋂ i ∈ I. A i)"

using h2 by simp

qed

section ‹4ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"

proof

show "s ∪ (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. A i ∪ s)"

proof

fix x

assume "x ∈ s ∪ (⋂ i ∈ I. A i)"

then show "x ∈ (⋂ i ∈ I. A i ∪ s)"

proof

assume "x ∈ s"

then show ?thesis by simp

assume "x ∈ (⋂ i ∈ I. A i)"

then show ?thesis by simp

qed

show "(⋂ i ∈ I. A i ∪ s) ⊆ s ∪ (⋂ i ∈ I. A i)"

proof

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i ∪ s)"

show "x ∈ s ∪ (⋂ i ∈ I. A i)"

proof (cases "x ∈ s")

case True

then show ?thesis by simp

case False

then show ?thesis using h2 by simp

qed

section ‹5ª demostración›

lemma "s ∪ (⋂ i ∈ I. A i) = (⋂ i ∈ I. A i ∪ s)"

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