La semana en Calculemus (9 de marzo de 2024)

Esta semana he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:

1. (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)
2. Pares ∪ Impares = Naturales
3. Los primos mayores que 2 son impares
4. s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)
5. (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

A continuación se muestran las soluciones.

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

Demostrar con Lean4 que
\[ (s \setminus t) ∪ (t \setminus s) = (s ∪ t) \setminus (s ∩ t) \]

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

import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

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

import Mathlib.Data.Set.Basic

open Set

variable {α : Type}

variable (s t : Set α)

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

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que, para todo \(x\),
\[ x ∈ (s \setminus t) ∪ (t \setminus s) ↔ x ∈ (s ∪ t) \setminus (s ∩ t) \]
Se demuestra mediante la siguiente cadena de equivalencias:
\begin{align}
&x ∈ (s \setminus t) ∪ (t \setminus s) \\
↔ &x ∈ (s \setminus t) ∨ x ∈ (t \setminus s) \\
↔ &(x ∈ s ∧ x ∉ t) ∨ x ∈ (t \setminus s) \\
↔ &(x ∈ s ∨ x ∈ (t \ s)) ∧ (x ∉ t ∨ x ∈ (t \setminus s)) \\
↔ &(x ∈ s ∨ (x ∈ t ∧ x ∉ s)) ∧ (x ∉ t ∨ (x ∈ t ∧ x ∉ s)) \\
↔ &((x ∈ s ∨ x ∈ t) ∧ (x ∈ s ∨ x ∉ s)) ∧ ((x ∉ t ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s)) \\
↔ &(x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s) \\
↔ &(x ∈ s ∪ t) ∧ (x ∉ t ∨ x ∉ s) \\
↔ &(x ∈ s ∪ t) ∧ (x ∉ s ∨ x ∉ t) \\
↔ &(x ∈ s ∪ t) ∧ ¬(x ∈ s ∧ x ∈ t) \\
↔ &(x ∈ s ∪ t) ∧ ¬(x ∈ s ∩ t) \\
↔ &x ∈ (s ∪ t) \setminus (s ∩ t)
\end{align}

2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  calc x ∈ (s \ t) ∪ (t \ s)
     ↔ x ∈ (s \ t) ∨ x ∈ (t \ s) :=
         by exact mem_union x (s \ t) (t \ s)
   _ ↔ (x ∈ s ∧ x ∉ t) ∨ x ∈ (t \ s) :=
         by simp only [mem_diff]
   _ ↔ (x ∈ s ∨ x ∈ (t \ s)) ∧ (x ∉ t ∨ x ∈ (t \ s)) :=
         by exact and_or_right
   _ ↔ (x ∈ s ∨ (x ∈ t ∧ x ∉ s)) ∧ (x ∉ t ∨ (x ∈ t ∧ x ∉ s)) :=
         by simp only [mem_diff]
   _ ↔ ((x ∈ s ∨ x ∈ t) ∧ (x ∈ s ∨ x ∉ s)) ∧
       ((x ∉ t ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s)) :=
         by simp_all only [or_and_left]
   _ ↔ ((x ∈ s ∨ x ∈ t) ∧ True) ∧
       (True ∧ (x ∉ t ∨ x ∉ s)) :=
         by simp only [em (x ∈ s), em' (x ∈ t)]
   _ ↔ (x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s) :=
         by simp only [and_true_iff (x ∈ s ∨ x ∈ t),
                       true_and_iff (¬x ∈ t ∨ ¬x ∈ s)]
   _ ↔ (x ∈ s ∪ t) ∧ (x ∉ t ∨ x ∉ s) :=
         by simp only [mem_union]
   _ ↔ (x ∈ s ∪ t) ∧ (x ∉ s ∨ x ∉ t) :=
         by simp only [or_comm]
   _ ↔ (x ∈ s ∪ t) ∧ ¬(x ∈ s ∧ x ∈ t) :=
         by simp only [not_and_or]
   _ ↔ (x ∈ s ∪ t) ∧ ¬(x ∈ s ∩ t) :=
         by simp only [mem_inter_iff]
   _ ↔ x ∈ (s ∪ t) \ (s ∩ t)     :=
         by simp only [mem_diff]

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  constructor
  . -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)
    rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩)
    . -- xs : x ∈ s
      -- xnt : ¬x ∈ t
      -- ⊢ x ∈ (s ∪ t) \ (s ∩ t)
      constructor
      . -- ⊢ x ∈ s ∪ t
        left
        -- ⊢ x ∈ s
        exact xs
      . -- ⊢ ¬x ∈ s ∩ t
        rintro ⟨-, xt⟩
        -- xt : x ∈ t
        -- ⊢ False
        exact xnt xt
    . -- xt : x ∈ t
      -- xns : ¬x ∈ s
      -- ⊢ x ∈ (s ∪ t) \ (s ∩ t)
      constructor
      . -- ⊢ x ∈ s ∪ t
        right
        -- ⊢ x ∈ t
        exact xt
      . -- ⊢ ¬x ∈ s ∩ t
        rintro ⟨xs, -⟩
        -- xs : x ∈ s
        -- ⊢ False
        exact xns xs
  . -- ⊢ x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s)
    rintro ⟨xs | xt, nxst⟩
    . -- xs : x ∈ s
      -- ⊢ x ∈ (s \ t) ∪ (t \ s)
      left
      -- ⊢ x ∈ s \ t
      use xs
      -- ⊢ ¬x ∈ t
      intro xt
      -- xt : x ∈ t
      -- ⊢ False
      apply nxst
      -- ⊢ x ∈ s ∩ t
      constructor
      . -- ⊢ x ∈ s
        exact xs
      . -- ⊢ x ∈ t
        exact xt
    . -- nxst : ¬x ∈ s ∩ t
      -- xt : x ∈ t
      -- ⊢ x ∈ (s \ t) ∪ (t \ s)
      right
      -- ⊢ x ∈ t \ s
      use xt
      -- ⊢ ¬x ∈ s
      intro xs
      -- xs : x ∈ s
      -- ⊢ False
      apply nxst
      -- ⊢ x ∈ s ∩ t
      constructor
      . -- ⊢ x ∈ s
        exact xs
      . -- ⊢ x ∈ t
        exact xt

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  constructor
  . -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)
    rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩)
    . -- xt : x ∈ t
      -- xns : ¬x ∈ s
      -- ⊢ x ∈ (s ∪ t) \ (s ∩ t)
      aesop
    . -- xt : x ∈ t
      -- xns : ¬x ∈ s
      -- ⊢ x ∈ (s ∪ t) \ (s ∩ t)
      aesop
  . rintro ⟨xs | xt, nxst⟩
    . -- xs : x ∈ s
      -- ⊢ x ∈ (s \ t) ∪ (t \ s)
      aesop
    . -- nxst : ¬x ∈ s ∩ t
      -- xt : x ∈ t
      -- ⊢ x ∈ (s \ t) ∪ (t \ s)
      aesop

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  constructor
  . -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)
    rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩) <;> aesop
  . -- ⊢ x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s)
    rintro ⟨xs | xt, nxst⟩ <;> aesop

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext
  constructor
  . aesop
  . aesop

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  ext
  constructor <;> aesop

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

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
by
  rw [ext_iff]
  -- ⊢ ∀ (x : α), x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  intro
  -- x : α
  -- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)
  rw [iff_def]
  -- ⊢ (x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)) ∧
  --   (x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s))
  aesop

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

-- variable (x : α)
-- variable (a b c : Prop)
-- #check (mem_union x s t : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t)
-- #check (mem_diff x : x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t)
-- #check (and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c))
-- #check (or_and_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c))
-- #check (em a : a ∨ ¬ a)
-- #check (em' a : ¬ a ∨ a)
-- #check (and_true_iff a : a ∧ True ↔ a)
-- #check (true_and_iff a : True ∧ a ↔ a)
-- #check (or_comm : a ∨ b ↔ b ∨ a)
-- #check (not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b)
-- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t)
-- #check (ext_iff : s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)
-- #check (iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a))

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

import Mathlib.Data.Set.Basic

open Set

variable {α : Type}

variable (s t : Set α)

-- 1ª demostración

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

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

ext x

-- x : α

-- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

calc x ∈ (s \ t) ∪ (t \ s)

↔ x ∈ (s \ t) ∨ x ∈ (t \ s) :=

by exact mem_union x (s \ t) (t \ s)

_ ↔ (x ∈ s ∧ x ∉ t) ∨ x ∈ (t \ s) :=

by simp only [mem_diff]

_ ↔ (x ∈ s ∨ x ∈ (t \ s)) ∧ (x ∉ t ∨ x ∈ (t \ s)) :=

by exact and_or_right

_ ↔ (x ∈ s ∨ (x ∈ t ∧ x ∉ s)) ∧ (x ∉ t ∨ (x ∈ t ∧ x ∉ s)) :=

by simp only [mem_diff]

_ ↔ ((x ∈ s ∨ x ∈ t) ∧ (x ∈ s ∨ x ∉ s)) ∧

((x ∉ t ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s)) :=

by simp_all only [or_and_left]

_ ↔ ((x ∈ s ∨ x ∈ t) ∧ True) ∧

(True ∧ (x ∉ t ∨ x ∉ s)) :=

by simp only [em (x ∈ s), em' (x ∈ t)]

_ ↔ (x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∉ s) :=

by simp only [and_true_iff (x ∈ s ∨ x ∈ t),

true_and_iff (¬x ∈ t ∨ ¬x ∈ s)]

_ ↔ (x ∈ s ∪ t) ∧ (x ∉ t ∨ x ∉ s) :=

by simp only [mem_union]

_ ↔ (x ∈ s ∪ t) ∧ (x ∉ s ∨ x ∉ t) :=

by simp only [or_comm]

_ ↔ (x ∈ s ∪ t) ∧ ¬(x ∈ s ∧ x ∈ t) :=

by simp only [not_and_or]

_ ↔ (x ∈ s ∪ t) ∧ ¬(x ∈ s ∩ t) :=

by simp only [mem_inter_iff]

_ ↔ x ∈ (s ∪ t) \ (s ∩ t) :=

by simp only [mem_diff]

-- 2ª demostración

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

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

ext x

-- x : α

-- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

constructor

. -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)

rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩)

. -- xs : x ∈ s

-- xnt : ¬x ∈ t

-- ⊢ x ∈ (s ∪ t) \ (s ∩ t)

constructor

. -- ⊢ x ∈ s ∪ t

left

-- ⊢ x ∈ s

exact xs

. -- ⊢ ¬x ∈ s ∩ t

rintro ⟨-, xt⟩

-- xt : x ∈ t

-- ⊢ False

exact xnt xt

. -- xt : x ∈ t

-- xns : ¬x ∈ s

-- ⊢ x ∈ (s ∪ t) \ (s ∩ t)

constructor

. -- ⊢ x ∈ s ∪ t

right

-- ⊢ x ∈ t

exact xt

. -- ⊢ ¬x ∈ s ∩ t

rintro ⟨xs, -⟩

-- xs : x ∈ s

-- ⊢ False

exact xns xs

. -- ⊢ x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s)

rintro ⟨xs | xt, nxst⟩

. -- xs : x ∈ s

-- ⊢ x ∈ (s \ t) ∪ (t \ s)

left

-- ⊢ x ∈ s \ t

use xs

-- ⊢ ¬x ∈ t

intro xt

-- xt : x ∈ t

-- ⊢ False

apply nxst

-- ⊢ x ∈ s ∩ t

constructor

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ t

exact xt

. -- nxst : ¬x ∈ s ∩ t

-- xt : x ∈ t

-- ⊢ x ∈ (s \ t) ∪ (t \ s)

right

-- ⊢ x ∈ t \ s

use xt

-- ⊢ ¬x ∈ s

intro xs

-- xs : x ∈ s

-- ⊢ False

apply nxst

-- ⊢ x ∈ s ∩ t

constructor

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ t

exact xt

-- 3ª demostración

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

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

ext x

-- x : α

-- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

constructor

. -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)

rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩)

. -- xt : x ∈ t

-- xns : ¬x ∈ s

-- ⊢ x ∈ (s ∪ t) \ (s ∩ t)

aesop

. -- xt : x ∈ t

-- xns : ¬x ∈ s

-- ⊢ x ∈ (s ∪ t) \ (s ∩ t)

aesop

. rintro ⟨xs | xt, nxst⟩

. -- xs : x ∈ s

-- ⊢ x ∈ (s \ t) ∪ (t \ s)

aesop

. -- nxst : ¬x ∈ s ∩ t

-- xt : x ∈ t

-- ⊢ x ∈ (s \ t) ∪ (t \ s)

aesop

-- 4ª demostración

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

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

ext x

-- x : α

-- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

constructor

. -- ⊢ x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)

rintro (⟨xs, xnt⟩ | ⟨xt, xns⟩) <;> aesop

. -- ⊢ x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s)

rintro ⟨xs | xt, nxst⟩ <;> aesop

-- 5ª demostración

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

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

ext

constructor

. aesop

-- 6ª demostración

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

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

ext

constructor <;> aesop

-- 7ª demostración

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

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

rw [ext_iff]

-- ⊢ ∀ (x : α), x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

intro

-- x : α

-- ⊢ x ∈ (s \ t) ∪ (t \ s) ↔ x ∈ (s ∪ t) \ (s ∩ t)

rw [iff_def]

-- ⊢ (x ∈ (s \ t) ∪ (t \ s) → x ∈ (s ∪ t) \ (s ∩ t)) ∧

-- (x ∈ (s ∪ t) \ (s ∩ t) → x ∈ (s \ t) ∪ (t \ s))

aesop

-- Lemas usados

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

-- variable (x : α)

-- variable (a b c : Prop)

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

-- #check (mem_diff x : x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t)

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

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

-- #check (em a : a ∨ ¬ a)

-- #check (em' a : ¬ a ∨ a)

-- #check (and_true_iff a : a ∧ True ↔ a)

-- #check (true_and_iff a : True ∧ a ↔ a)

-- #check (or_comm : a ∨ b ↔ b ∨ a)

-- #check (not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b)

-- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t)

-- #check (ext_iff : s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)

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

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

3. Demostraciones con Isabelle/HOL

theory Diferencia_de_union_e_interseccion
imports Main
begin

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

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

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

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

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

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

theory Diferencia_de_union_e_interseccion

imports Main

begin

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

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

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

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

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

(* 6ª demostración *)

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

by auto

end

2. Pares ∪ Impares = Naturales

Los conjuntos de los números naturales, de los pares y de los impares se definen en Lean4 por

   def Naturales : Set ℕ := {n | True}
   def Pares     : Set ℕ := {n | Even n}
   def Impares   : Set ℕ := {n | ¬Even n}

def Naturales : Set ℕ := {n | True}

def Pares : Set ℕ := {n | Even n}

def Impares : Set ℕ := {n | ¬Even n}

Demostrar con Lean4 que

   Pares ∪ Impares = Naturales

1	Pares ∪ Impares = Naturales

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

import Mathlib.Data.Nat.Parity
open Set

def Naturales : Set ℕ := {n | True}
def Pares     : Set ℕ := {n | Even n}
def Impares   : Set ℕ := {n | ¬Even n}

example : Pares ∪ Impares = Naturales :=
by sorry

import Mathlib.Data.Nat.Parity

open Set

def Naturales : Set ℕ := {n | True}

def Pares : Set ℕ := {n | Even n}

def Impares : Set ℕ := {n | ¬Even n}

example : Pares ∪ Impares = Naturales :=

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que
\[ \{n | \text{Even}(n)\} ∪ \{n | ¬\text{Even}(n)\} = \{n | \text{True}\} \]
es decir,
\[ n ∈ \{n | \text{Even}(n)\} ∪ \{n | ¬\text{Even}(n)\} ↔ n ∈ \{n | \text{True}\} \]
que se reduce a
\[ ⊢ \text{Even}(n) ∨ ¬\text{Even}(n) \]
que es una tautología.

2. Demostraciones con Lean4

import Mathlib.Data.Nat.Parity
open Set

def Naturales : Set ℕ := {n | True}
def Pares     : Set ℕ := {n | Even n}
def Impares   : Set ℕ := {n | ¬Even n}

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

example : Pares ∪ Impares = Naturales :=
by
  unfold Pares Impares Naturales
  -- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True}
  ext n
  -- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True}
  simp
  -- ⊢ Even n ∨ ¬Even n
  exact em (Even n)

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

example : Pares ∪ Impares = Naturales :=
by
  unfold Pares Impares Naturales
  -- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True}
  ext n
  -- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True}
  tauto

import Mathlib.Data.Nat.Parity

open Set

def Naturales : Set ℕ := {n | True}

def Pares : Set ℕ := {n | Even n}

def Impares : Set ℕ := {n | ¬Even n}

-- 1ª demostración

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

example : Pares ∪ Impares = Naturales :=

unfold Pares Impares Naturales

-- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True}

ext n

-- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True}

simp

-- ⊢ Even n ∨ ¬Even n

exact em (Even n)

-- 2ª demostración

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

example : Pares ∪ Impares = Naturales :=

unfold Pares Impares Naturales

-- ⊢ {n | Even n} ∪ {n | ¬Even n} = {n | True}

ext n

-- ⊢ n ∈ {n | Even n} ∪ {n | ¬Even n} ↔ n ∈ {n | True}

tauto

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

3. Demostraciones con Isabelle/HOL

theory Union_de_pares_e_impares
imports Main
begin

definition naturales :: "nat set" where
  "naturales = {n∈ℕ . True}"

definition pares :: "nat set" where
  "pares = {n∈ℕ . even n}"

definition impares :: "nat set" where
  "impares = {n∈ℕ . ¬ even n}"

(* 1ª demostración *)
lemma "pares ∪ impares = naturales"
proof -
  have "∀ n ∈ ℕ . even n ∨ ¬ even n ⟷ True"
    by simp
  then have "{n ∈ ℕ. even n} ∪ {n ∈ ℕ. ¬ even n} = {n ∈ ℕ. True}"
    by auto
  then show "pares ∪ impares = naturales"
    by (simp add: naturales_def pares_def impares_def)
qed

(* 2ª demostración *)
lemma "pares ∪ impares = naturales"
  unfolding naturales_def pares_def impares_def
  by auto

end

theory Union_de_pares_e_impares

imports Main

begin

definition naturales :: "nat set" where

"naturales = {n∈ℕ . True}"

definition pares :: "nat set" where

"pares = {n∈ℕ . even n}"

definition impares :: "nat set" where

"impares = {n∈ℕ . ¬ even n}"

(* 1ª demostración *)

lemma "pares ∪ impares = naturales"

proof -

have "∀ n ∈ ℕ . even n ∨ ¬ even n ⟷ True"

by simp

then have "{n ∈ ℕ. even n} ∪ {n ∈ ℕ. ¬ even n} = {n ∈ ℕ. True}"

by auto

then show "pares ∪ impares = naturales"

by (simp add: naturales_def pares_def impares_def)

qed

(* 2ª demostración *)

lemma "pares ∪ impares = naturales"

unfolding naturales_def pares_def impares_def

by auto

end

3. Los primos mayores que 2 son impares

Los números primos, los mayores que 2 y los impares se definen en Lean4 por

   def Primos      : Set ℕ := {n | Nat.Prime n}
   def MayoresQue2 : Set ℕ := {n | n > 2}
   def Impares     : Set ℕ := {n | ¬Even n}

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

Demostrar con Lean4 que

   Primos ∩ MayoresQue2 ⊆ Impares

1	Primos ∩ MayoresQue2 ⊆ Impares

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

import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

open Nat

def Primos      : Set ℕ := {n | Nat.Prime n}
def MayoresQue2 : Set ℕ := {n | n > 2}
def Impares     : Set ℕ := {n | ¬Even n}

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by sorry

import Mathlib.Data.Nat.Parity

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

open Nat

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

example : Primos ∩ MayoresQue2 ⊆ Impares :=

by sorry

1. Demostraciones con Lean4

import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

open Nat

def Primos      : Set ℕ := {n | Nat.Prime n}
def MayoresQue2 : Set ℕ := {n | n > 2}
def Impares     : Set ℕ := {n | ¬Even n}

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  intro n
  -- n : ℕ
  -- ⊢ n ∈ {n | Nat.Prime n} ∩ {n | n > 2} → n ∈ {n | ¬Even n}
  simp
  -- ⊢ Nat.Prime n → 2 < n → ¬Even n
  intro hn
  -- hn : Nat.Prime n
  -- ⊢ 2 < n → ¬Even n
  rcases Prime.eq_two_or_odd hn with (h | h)
  . -- h : n = 2
    rw [h]
    -- ⊢ 2 < 2 → ¬Even 2
    intro h1
    -- h1 : 2 < 2
    -- ⊢ ¬Even 2
    exfalso
    exact absurd h1 (lt_irrefl 2)
  . -- h : n % 2 = 1
    rw [even_iff]
    -- ⊢ 2 < n → ¬n % 2 = 0
    rw [h]
    -- ⊢ 2 < n → ¬1 = 0
    intro
    -- a : 2 < n
    -- ⊢ ¬1 = 0
    exact one_ne_zero

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  rintro n ⟨h1, h2⟩
  -- n : ℕ
  -- h1 : n ∈ {n | Nat.Prime n}
  -- h2 : n ∈ {n | n > 2}
  -- ⊢ n ∈ {n | ¬Even n}
  simp at *
  -- h1 : Nat.Prime n
  -- h2 : 2 < n
  -- ⊢ ¬Even n
  rcases Prime.eq_two_or_odd h1 with (h3 | h4)
  . -- h3 : n = 2
    rw [h3] at h2
    -- h2 : 2 < 2
    exfalso
    -- ⊢ False
    exact absurd h2 (lt_irrefl 2)
  . -- h4 : n % 2 = 1
    rw [even_iff]
    -- ⊢ ¬n % 2 = 0
    rw [h4]
    -- ⊢ ¬1 = 0
    exact one_ne_zero

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=
by
  unfold Primos MayoresQue2 Impares
  -- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}
  rintro n ⟨h1, h2⟩
  -- n : ℕ
  -- h1 : n ∈ {n | Nat.Prime n}
  -- h2 : n ∈ {n | n > 2}
  -- ⊢ n ∈ {n | ¬Even n}
  simp at *
  -- h1 : Nat.Prime n
  -- h2 : 2 < n
  -- ⊢ ¬Even n
  rcases Prime.eq_two_or_odd h1 with (h3 | h4)
  . -- h3 : n = 2
    rw [h3] at h2
    -- h2 : 2 < 2
    linarith
  . -- h4 : n % 2 = 1
    rw [even_iff]
    -- ⊢ ¬n % 2 = 0
    linarith

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

-- variable (p n : ℕ)
-- variable (a b : Prop)
-- #check (Prime.eq_two_or_odd : Nat.Prime p → p = 2 ∨ p % 2 = 1)
-- #check (absurd : a → ¬a → b)
-- #check (even_iff : Even n ↔ n % 2 = 0)
-- #check (lt_irrefl n : ¬n < n)
-- #check (one_ne_zero : 1 ≠ 0)

100

101

102

103

104

105

106

107

108

109

110

import Mathlib.Data.Nat.Parity

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

open Nat

def Primos : Set ℕ := {n | Nat.Prime n}

def MayoresQue2 : Set ℕ := {n | n > 2}

def Impares : Set ℕ := {n | ¬Even n}

-- 1ª demostración

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

intro n

-- n : ℕ

-- ⊢ n ∈ {n | Nat.Prime n} ∩ {n | n > 2} → n ∈ {n | ¬Even n}

simp

-- ⊢ Nat.Prime n → 2 < n → ¬Even n

intro hn

-- hn : Nat.Prime n

-- ⊢ 2 < n → ¬Even n

rcases Prime.eq_two_or_odd hn with (h | h)

. -- h : n = 2

rw [h]

-- ⊢ 2 < 2 → ¬Even 2

intro h1

-- h1 : 2 < 2

-- ⊢ ¬Even 2

exfalso

exact absurd h1 (lt_irrefl 2)

. -- h : n % 2 = 1

rw [even_iff]

-- ⊢ 2 < n → ¬n % 2 = 0

rw [h]

-- ⊢ 2 < n → ¬1 = 0

intro

-- a : 2 < n

-- ⊢ ¬1 = 0

exact one_ne_zero

-- 2ª demostración

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

rintro n ⟨h1, h2⟩

-- n : ℕ

-- h1 : n ∈ {n | Nat.Prime n}

-- h2 : n ∈ {n | n > 2}

-- ⊢ n ∈ {n | ¬Even n}

simp at *

-- h1 : Nat.Prime n

-- h2 : 2 < n

-- ⊢ ¬Even n

rcases Prime.eq_two_or_odd h1 with (h3 | h4)

. -- h3 : n = 2

rw [h3] at h2

-- h2 : 2 < 2

exfalso

-- ⊢ False

exact absurd h2 (lt_irrefl 2)

. -- h4 : n % 2 = 1

rw [even_iff]

-- ⊢ ¬n % 2 = 0

rw [h4]

-- ⊢ ¬1 = 0

exact one_ne_zero

-- 3ª demostración

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

example : Primos ∩ MayoresQue2 ⊆ Impares :=

unfold Primos MayoresQue2 Impares

-- ⊢ {n | Nat.Prime n} ∩ {n | n > 2} ⊆ {n | ¬Even n}

rintro n ⟨h1, h2⟩

-- n : ℕ

-- h1 : n ∈ {n | Nat.Prime n}

-- h2 : n ∈ {n | n > 2}

-- ⊢ n ∈ {n | ¬Even n}

simp at *

-- h1 : Nat.Prime n

-- h2 : 2 < n

-- ⊢ ¬Even n

rcases Prime.eq_two_or_odd h1 with (h3 | h4)

. -- h3 : n = 2

rw [h3] at h2

-- h2 : 2 < 2

linarith

. -- h4 : n % 2 = 1

rw [even_iff]

-- ⊢ ¬n % 2 = 0

linarith

-- Lemas usados

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

-- variable (p n : ℕ)

-- variable (a b : Prop)

-- #check (Prime.eq_two_or_odd : Nat.Prime p → p = 2 ∨ p % 2 = 1)

-- #check (absurd : a → ¬a → b)

-- #check (even_iff : Even n ↔ n % 2 = 0)

-- #check (lt_irrefl n : ¬n < n)

-- #check (one_ne_zero : 1 ≠ 0)

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

3. Demostraciones con Isabelle/HOL

theory Interseccion_de_los_primos_y_los_mayores_que_dos
imports Main "HOL-Number_Theory.Number_Theory"
begin

definition primos :: "nat set" where
  "primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where
  "mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where
  "impares = {n ∈ ℕ . ¬ even n}"

(* 1ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
proof
  fix x
  assume "x ∈ primos ∩ mayoresQue2"
  then have "x ∈ ℕ ∧ prime x ∧ 2 < x"
    by (simp add: primos_def mayoresQue2_def)
  then have "x ∈ ℕ ∧ odd x"
    by (simp add: prime_odd_nat)
  then show "x ∈ impares"
    by (simp add: impares_def)
qed

(* 2ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (simp add: Collect_mono_iff Int_def prime_odd_nat)

(* 3ª demostración *)
lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (auto simp add: prime_odd_nat)

end

theory Interseccion_de_los_primos_y_los_mayores_que_dos

imports Main "HOL-Number_Theory.Number_Theory"

begin

definition primos :: "nat set" where

"primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where

"mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where

"impares = {n ∈ ℕ . ¬ even n}"

(* 1ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

proof

fix x

assume "x ∈ primos ∩ mayoresQue2"

then have "x ∈ ℕ ∧ prime x ∧ 2 < x"

by (simp add: primos_def mayoresQue2_def)

then have "x ∈ ℕ ∧ odd x"

by (simp add: prime_odd_nat)

then show "x ∈ impares"

by (simp add: impares_def)

qed

(* 2ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (simp add: Collect_mono_iff Int_def prime_odd_nat)

(* 3ª demostración *)

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (auto simp add: prime_odd_nat)

end

4. s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)

Demostrar con Lean4 que
\[ s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s : Set α)

variable (A : ℕ → Set α)

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que para cada \(x\), se verifica que
\[ x ∈ s ∩ ⋃_i A_i ↔ x ∈ ⋃_i A_i ∩ s \]
Lo demostramos mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ s ∩ ⋃_i A_i &↔ x ∈ s ∧ x ∈ ⋃_i A_i \\
&↔ x ∈ s ∧ (∃ i)[x ∈ A_i] \\
&↔ (∃ i)[x ∈ s ∧ x ∈ A_i] \\
&↔ (∃ i)[x ∈ A_i ∧ x ∈ s] \\
&↔ (∃ i)[x ∈ A_i ∩ s] \\
&↔ x ∈ ⋃_i (A i ∩ s)
\end{align}

2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s
  calc x ∈ s ∩ ⋃ (i : ℕ), A i
     ↔ x ∈ s ∧ x ∈ ⋃ (i : ℕ), A i :=
         by simp only [mem_inter_iff]
   _ ↔ x ∈ s ∧ (∃ i : ℕ, x ∈ A i) :=
         by simp only [mem_iUnion]
   _ ↔ ∃ i : ℕ, x ∈ s ∧ x ∈ A i :=
         by simp only [exists_and_left]
   _ ↔ ∃ i : ℕ, x ∈ A i ∧ x ∈ s :=
         by simp only [and_comm]
   _ ↔ ∃ i : ℕ, x ∈ A i ∩ s :=
         by simp only [mem_inter_iff]
   _ ↔ x ∈ ⋃ (i : ℕ), A i ∩ s :=
         by simp only [mem_iUnion]

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s
  constructor
  . -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i → x ∈ ⋃ (i : ℕ), A i ∩ s
    intro h
    -- h : x ∈ s ∩ ⋃ (i : ℕ), A i
    -- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s
    rw [mem_iUnion]
    -- ⊢ ∃ i, x ∈ A i ∩ s
    rcases h with ⟨xs, xUAi⟩
    -- xs : x ∈ s
    -- xUAi : x ∈ ⋃ (i : ℕ), A i
    rw [mem_iUnion] at xUAi
    -- xUAi : ∃ i, x ∈ A i
    rcases xUAi with ⟨i, xAi⟩
    -- i : ℕ
    -- xAi : x ∈ A i
    use i
    -- ⊢ x ∈ A i ∩ s
    constructor
    . -- ⊢ x ∈ A i
      exact xAi
    . -- ⊢ x ∈ s
      exact xs
  . -- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s → x ∈ s ∩ ⋃ (i : ℕ), A i
    intro h
    -- h : x ∈ ⋃ (i : ℕ), A i ∩ s
    -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i
    rw [mem_iUnion] at h
    -- h : ∃ i, x ∈ A i ∩ s
    rcases h with ⟨i, hi⟩
    -- i : ℕ
    -- hi : x ∈ A i ∩ s
    rcases hi with ⟨xAi, xs⟩
    -- xAi : x ∈ A i
    -- xs : x ∈ s
    constructor
    . -- ⊢ x ∈ s
      exact xs
    . -- ⊢ x ∈ ⋃ (i : ℕ), A i
      rw [mem_iUnion]
      -- ⊢ ∃ i, x ∈ A i
      use i
      -- ⊢ x ∈ A i
      exact xAi

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s
  simp
  -- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) ↔ (∃ i, x ∈ A i) ∧ x ∈ s
  constructor
  . -- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) → (∃ i, x ∈ A i) ∧ x ∈ s
    rintro ⟨xs, ⟨i, xAi⟩⟩
    -- xs : x ∈ s
    -- i : ℕ
    -- xAi : x ∈ A i
    -- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s
    exact ⟨⟨i, xAi⟩, xs⟩
  . -- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s → x ∈ s ∧ ∃ i, x ∈ A i
    rintro ⟨⟨i, xAi⟩, xs⟩
    -- xs : x ∈ s
    -- i : ℕ
    -- xAi : x ∈ A i
    -- ⊢ x ∈ s ∧ ∃ i, x ∈ A i
    exact ⟨xs, ⟨i, xAi⟩⟩

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s
  aesop

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by ext; aesop

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

-- variable (x : α)
-- variable (t : Set α)
-- variable (a b : Prop)
-- variable (p : α → Prop)
-- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i)
-- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t)
-- #check (exists_and_left : (∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x)
-- #check (and_comm : a ∧ b ↔ b ∧ a)

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

import Mathlib.Data.Set.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s : Set α)

variable (A : ℕ → Set α)

-- 1ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

ext x

-- x : α

-- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s

calc x ∈ s ∩ ⋃ (i : ℕ), A i

↔ x ∈ s ∧ x ∈ ⋃ (i : ℕ), A i :=

by simp only [mem_inter_iff]

_ ↔ x ∈ s ∧ (∃ i : ℕ, x ∈ A i) :=

by simp only [mem_iUnion]

_ ↔ ∃ i : ℕ, x ∈ s ∧ x ∈ A i :=

by simp only [exists_and_left]

_ ↔ ∃ i : ℕ, x ∈ A i ∧ x ∈ s :=

by simp only [and_comm]

_ ↔ ∃ i : ℕ, x ∈ A i ∩ s :=

by simp only [mem_inter_iff]

_ ↔ x ∈ ⋃ (i : ℕ), A i ∩ s :=

by simp only [mem_iUnion]

-- 2ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

ext x

-- x : α

-- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s

constructor

. -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i → x ∈ ⋃ (i : ℕ), A i ∩ s

intro h

-- h : x ∈ s ∩ ⋃ (i : ℕ), A i

-- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s

rw [mem_iUnion]

-- ⊢ ∃ i, x ∈ A i ∩ s

rcases h with ⟨xs, xUAi⟩

-- xs : x ∈ s

-- xUAi : x ∈ ⋃ (i : ℕ), A i

rw [mem_iUnion] at xUAi

-- xUAi : ∃ i, x ∈ A i

rcases xUAi with ⟨i, xAi⟩

-- i : ℕ

-- xAi : x ∈ A i

use i

-- ⊢ x ∈ A i ∩ s

constructor

. -- ⊢ x ∈ A i

exact xAi

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s → x ∈ s ∩ ⋃ (i : ℕ), A i

intro h

-- h : x ∈ ⋃ (i : ℕ), A i ∩ s

-- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i

rw [mem_iUnion] at h

-- h : ∃ i, x ∈ A i ∩ s

rcases h with ⟨i, hi⟩

-- i : ℕ

-- hi : x ∈ A i ∩ s

rcases hi with ⟨xAi, xs⟩

-- xAi : x ∈ A i

-- xs : x ∈ s

constructor

. -- ⊢ x ∈ s

exact xs

. -- ⊢ x ∈ ⋃ (i : ℕ), A i

rw [mem_iUnion]

-- ⊢ ∃ i, x ∈ A i

use i

-- ⊢ x ∈ A i

exact xAi

-- 3ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

ext x

-- x : α

-- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s

simp

-- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) ↔ (∃ i, x ∈ A i) ∧ x ∈ s

constructor

. -- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) → (∃ i, x ∈ A i) ∧ x ∈ s

rintro ⟨xs, ⟨i, xAi⟩⟩

-- xs : x ∈ s

-- i : ℕ

-- xAi : x ∈ A i

-- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s

exact ⟨⟨i, xAi⟩, xs⟩

. -- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s → x ∈ s ∧ ∃ i, x ∈ A i

rintro ⟨⟨i, xAi⟩, xs⟩

-- xs : x ∈ s

-- i : ℕ

-- xAi : x ∈ A i

-- ⊢ x ∈ s ∧ ∃ i, x ∈ A i

exact ⟨xs, ⟨i, xAi⟩⟩

-- 3ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

ext x

-- x : α

-- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s

aesop

-- 4ª demostración

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

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by ext; aesop

-- Lemas usados

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

-- variable (x : α)

-- variable (t : Set α)

-- variable (a b : Prop)

-- variable (p : α → Prop)

-- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i)

-- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t)

-- #check (exists_and_left : (∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x)

-- #check (and_comm : a ∧ b ↔ b ∧ a)

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

3. Demostraciones con Isabelle/HOL

theory Distributiva_de_la_interseccion_respecto_de_la_union_general
imports Main
begin

(* 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 have "x ∈ s"
      by (simp only: IntD1)
    have "x ∈ (⋃ i ∈ I. A i)"
      using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by (simp only: IntD2)
    then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ A i"
      then have "x ∈ A i ∩ s"
        using ‹x ∈ s› by (rule IntI)
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋃ i ∈ I. A i ∩ s)"
    then show "x ∈ s ∩ (⋃ i ∈ I. A i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ A i ∩ s"
      then have "x ∈ A i"
        by (rule IntD1)
      have "x ∈ s"
        using ‹x ∈ A i ∩ s› by (rule IntD2)
      moreover
      have "x ∈ (⋃ i ∈ I. A i)"
        using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)
      ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"
        by (rule IntI)
    qed
  qed
qed

(* 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 have "x ∈ s"
      by simp
    have "x ∈ (⋃ i ∈ I. A i)"
      using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by simp
    then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ A i"
      then have "x ∈ A i ∩ s"
        using ‹x ∈ s› by simp
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"
  proof
    fix x
    assume "x ∈ (⋃ i ∈ I. A i ∩ s)"
    then show "x ∈ s ∩ (⋃ i ∈ I. A i)"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ A i ∩ s"
      then have "x ∈ A i"
        by simp
      have "x ∈ s"
        using ‹x ∈ A i ∩ s› by simp
      moreover
      have "x ∈ (⋃ i ∈ I. A i)"
        using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)
      ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"
        by simp
    qed
  qed
qed

(* 3ª demostración *)
lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"
  by auto

end

theory Distributiva_de_la_interseccion_respecto_de_la_union_general

imports Main

begin

(* 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 have "x ∈ s"

by (simp only: IntD1)

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

using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by (simp only: IntD2)

then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "x ∈ A i ∩ s"

using ‹x ∈ s› by (rule IntI)

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

by (rule UN_I)

qed

show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"

proof (rule subsetI)

fix x

assume "x ∈ (⋃ i ∈ I. A i ∩ s)"

then show "x ∈ s ∩ (⋃ i ∈ I. A i)"

proof (rule UN_E)

fix i

assume "i ∈ I"

assume "x ∈ A i ∩ s"

then have "x ∈ A i"

by (rule IntD1)

have "x ∈ s"

using ‹x ∈ A i ∩ s› by (rule IntD2)

moreover

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

using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)

ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"

by (rule IntI)

qed

(* 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 have "x ∈ s"

by simp

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

using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by simp

then show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

proof

fix i

assume "i ∈ I"

assume "x ∈ A i"

then have "x ∈ A i ∩ s"

using ‹x ∈ s› by simp

with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))"

by (rule UN_I)

qed

show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)"

proof

fix x

assume "x ∈ (⋃ i ∈ I. A i ∩ s)"

then show "x ∈ s ∩ (⋃ i ∈ I. A i)"

proof

fix i

assume "i ∈ I"

assume "x ∈ A i ∩ s"

then have "x ∈ A i"

by simp

have "x ∈ s"

using ‹x ∈ A i ∩ s› by simp

moreover

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

using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I)

ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)"

by simp

qed

(* 3ª demostración *)

lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))"

by auto

end

5. (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

Demostrar con Lean4 que
\[ ⋂_i (A_i ∩ B_i) = (⋂_i A_i) ∩ (⋂_i B_i) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (A B : ℕ → Set α)

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (A B : ℕ → Set α)

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que para \(x\) se verifica
\[ x ∈ ⋂_i (A_i ∩ B_i) ↔ x ∈ (⋂_i A_i) ∩ (⋂_i B_i) \]
Lo demostramos mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ ⋂_i (A_i ∩ B_i) &↔ (∀ i)[x ∈ A_i ∩ B_i] \\
&↔ (∀ i)[x ∈ A_i ∧ x ∈ B_i] \\
&↔ (∀ i)[x ∈ A_i] ∧ (∀ i)[x ∈ B_i] \\
&↔ x ∈ (⋂_i A_i) ∧ x ∈ (⋂_i B_i) \\
&↔ x ∈ (⋂_i A_i) ∩ (⋂_i B_i)
\end{align}

2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (A B : ℕ → Set α)

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i
  calc x ∈ ⋂ i, A i ∩ B i
     ↔ ∀ i, x ∈ A i ∩ B i :=
         by exact mem_iInter
   _ ↔ ∀ i, x ∈ A i ∧ x ∈ B i :=
         by simp only [mem_inter_iff]
   _ ↔ (∀ i, x ∈ A i) ∧ (∀ i, x ∈ B i) :=
         by exact forall_and
   _ ↔ x ∈ (⋂ i, A i) ∧ x ∈ (⋂ i, B i) :=
         by simp only [mem_iInter]
   _ ↔ x ∈ (⋂ i, A i) ∩ ⋂ i, B i :=
         by simp only [mem_inter_iff]

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i
  simp only [mem_inter_iff, mem_iInter]
  -- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
  constructor
  . -- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) → (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
    intro h
    -- h : ∀ (i : ℕ), x ∈ A i ∧ x ∈ B i
    -- ⊢ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
    constructor
    . -- ⊢ ∀ (i : ℕ), x ∈ A i
      intro i
      -- i : ℕ
      -- ⊢ x ∈ A i
      exact (h i).1
    . -- ⊢ ∀ (i : ℕ), x ∈ B i
      intro i
      -- i : ℕ
      -- ⊢ x ∈ B i
      exact (h i).2
  . -- ⊢ ((∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i) → ∀ (i : ℕ), x ∈ A i ∧ x ∈ B i
    intros h i
    -- h : (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
    -- i : ℕ
    -- ⊢ x ∈ A i ∧ x ∈ B i
    rcases h with ⟨h1, h2⟩
    -- h1 : ∀ (i : ℕ), x ∈ A i
    -- h2 : ∀ (i : ℕ), x ∈ B i
    constructor
    . -- ⊢ x ∈ A i
      exact h1 i
    . -- ⊢ x ∈ B i
      exact h2 i

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i
  simp only [mem_inter_iff, mem_iInter]
  -- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
  exact ⟨fun h ↦ ⟨fun i ↦ (h i).1, fun i ↦ (h i).2⟩,
         fun ⟨h1, h2⟩ i ↦ ⟨h1 i, h2 i⟩⟩

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by
  ext
  -- x : α
  -- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i
  simp only [mem_inter_iff, mem_iInter]
  -- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i
  aesop

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

-- variable (x : α)
-- variable (a b : Set α)
-- variable (ι : Sort v)
-- variable (s : ι → Set α)
-- variable (p q : α → Prop)
-- #check (forall_and : (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x)
-- #check (mem_iInter : x ∈ ⋂ (i : ι), s i ↔ ∀ (i : ι), x ∈ s i)
-- #check (mem_inter_iff x a b : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b)

100

101

102

103

104

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (A B : ℕ → Set α)

-- 1ª demostración

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext x

-- x : α

-- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i

calc x ∈ ⋂ i, A i ∩ B i

↔ ∀ i, x ∈ A i ∩ B i :=

by exact mem_iInter

_ ↔ ∀ i, x ∈ A i ∧ x ∈ B i :=

by simp only [mem_inter_iff]

_ ↔ (∀ i, x ∈ A i) ∧ (∀ i, x ∈ B i) :=

by exact forall_and

_ ↔ x ∈ (⋂ i, A i) ∧ x ∈ (⋂ i, B i) :=

by simp only [mem_iInter]

_ ↔ x ∈ (⋂ i, A i) ∩ ⋂ i, B i :=

by simp only [mem_inter_iff]

-- 2ª demostración

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext x

-- x : α

-- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i

simp only [mem_inter_iff, mem_iInter]

-- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

constructor

. -- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) → (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

intro h

-- h : ∀ (i : ℕ), x ∈ A i ∧ x ∈ B i

-- ⊢ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

constructor

. -- ⊢ ∀ (i : ℕ), x ∈ A i

intro i

-- i : ℕ

-- ⊢ x ∈ A i

exact (h i).1

. -- ⊢ ∀ (i : ℕ), x ∈ B i

intro i

-- i : ℕ

-- ⊢ x ∈ B i

exact (h i).2

. -- ⊢ ((∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i) → ∀ (i : ℕ), x ∈ A i ∧ x ∈ B i

intros h i

-- h : (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

-- i : ℕ

-- ⊢ x ∈ A i ∧ x ∈ B i

rcases h with ⟨h1, h2⟩

-- h1 : ∀ (i : ℕ), x ∈ A i

-- h2 : ∀ (i : ℕ), x ∈ B i

constructor

. -- ⊢ x ∈ A i

exact h1 i

. -- ⊢ x ∈ B i

exact h2 i

-- 3ª demostración

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext x

-- x : α

-- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i

simp only [mem_inter_iff, mem_iInter]

-- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

exact ⟨fun h ↦ ⟨fun i ↦ (h i).1, fun i ↦ (h i).2⟩,

fun ⟨h1, h2⟩ i ↦ ⟨h1 i, h2 i⟩⟩

-- 4ª demostración

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

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

ext

-- x : α

-- ⊢ x ∈ ⋂ (i : ℕ), A i ∩ B i ↔ x ∈ (⋂ (i : ℕ), A i) ∩ ⋂ (i : ℕ), B i

simp only [mem_inter_iff, mem_iInter]

-- ⊢ (∀ (i : ℕ), x ∈ A i ∧ x ∈ B i) ↔ (∀ (i : ℕ), x ∈ A i) ∧ ∀ (i : ℕ), x ∈ B i

aesop

-- Lemas usados

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

-- variable (x : α)

-- variable (a b : Set α)

-- variable (ι : Sort v)

-- variable (s : ι → Set α)

-- variable (p q : α → Prop)

-- #check (forall_and : (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x)

-- #check (mem_iInter : x ∈ ⋂ (i : ι), s i ↔ ∀ (i : ι), x ∈ s i)

-- #check (mem_inter_iff x a b : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b)

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

3. Demostraciones con Isabelle/HOL

theory Interseccion_de_intersecciones
imports Main
begin

(* 1ª demostración *)
lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
proof (rule equalityI)
  show "(⋂ i ∈ I. A i ∩ B i) ⊆ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume h1 : "x ∈ (⋂ i ∈ I. A i ∩ B i)"
    have "x ∈ (⋂ i ∈ I. A i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with h1 have "x ∈ A i ∩ B i"
        by (rule INT_D)
      then show "x ∈ A i"
        by (rule IntD1)
    qed
    moreover
    have "x ∈ (⋂ i ∈ I. B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with h1 have "x ∈ A i ∩ B i"
        by (rule INT_D)
      then show "x ∈ B i"
        by (rule IntD2)
    qed
    ultimately show "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
      by (rule IntI)
  qed
next
  show "(⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. A i ∩ B i)"
  proof (rule subsetI)
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. A i ∩ B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      have "x ∈ A i"
      proof -
        have "x ∈ (⋂ i ∈ I. A i)"
          using h2 by (rule IntD1)
        then show "x ∈ A i"
          using ‹i ∈ I› by (rule INT_D)
      qed
      moreover
      have "x ∈ B i"
      proof -
        have "x ∈ (⋂ i ∈ I. B i)"
          using h2 by (rule IntD2)
        then show "x ∈ B i"
          using ‹i ∈ I› by (rule INT_D)
      qed
      ultimately show "x ∈ A i ∩ B i"
        by (rule IntI)
    qed
  qed
qed

(* 2ª demostración *)
lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
proof
  show "(⋂ i ∈ I. A i ∩ B i) ⊆ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
  proof
    fix x
    assume h1 : "x ∈ (⋂ i ∈ I. A i ∩ B i)"
    have "x ∈ (⋂ i ∈ I. A i)"
    proof
      fix i
      assume "i ∈ I"
      then show "x ∈ A i"
        using h1 by simp
    qed
    moreover
    have "x ∈ (⋂ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      then show "x ∈ B i"
        using h1 by simp
    qed
    ultimately show "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
      by simp
  qed
next
  show "(⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. A i ∩ B i)"
  proof
    fix x
    assume h2 : "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. A i ∩ B i)"
    proof
      fix i
      assume "i ∈ I"
      then have "x ∈ A i"
        using h2 by simp
      moreover
      have "x ∈ B i"
        using ‹i ∈ I› h2 by simp
      ultimately show "x ∈ A i ∩ B i"
        by simp
    qed
qed
qed

(* 3ª demostración *)
lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"
  by auto

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

theory Interseccion_de_intersecciones

imports Main

begin

(* 1ª demostración *)

lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

proof (rule equalityI)

show "(⋂ i ∈ I. A i ∩ B i) ⊆ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

proof (rule subsetI)

fix x

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

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

proof (rule INT_I)

fix i

assume "i ∈ I"

with h1 have "x ∈ A i ∩ B i"

by (rule INT_D)

then show "x ∈ A i"

by (rule IntD1)

qed

moreover

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

proof (rule INT_I)

fix i

assume "i ∈ I"

with h1 have "x ∈ A i ∩ B i"

by (rule INT_D)

then show "x ∈ B i"

by (rule IntD2)

qed

ultimately show "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

by (rule IntI)

qed

show "(⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. A i ∩ B i)"

proof (rule subsetI)

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. A i ∩ B i)"

proof (rule INT_I)

fix i

assume "i ∈ I"

have "x ∈ A i"

proof -

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

using h2 by (rule IntD1)

then show "x ∈ A i"

using ‹i ∈ I› by (rule INT_D)

qed

moreover

have "x ∈ B i"

proof -

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

using h2 by (rule IntD2)

then show "x ∈ B i"

using ‹i ∈ I› by (rule INT_D)

qed

ultimately show "x ∈ A i ∩ B i"

by (rule IntI)

qed

(* 2ª demostración *)

lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

proof

show "(⋂ i ∈ I. A i ∩ B i) ⊆ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

proof

fix x

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

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

proof

fix i

assume "i ∈ I"

then show "x ∈ A i"

using h1 by simp

qed

moreover

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

proof

fix i

assume "i ∈ I"

then show "x ∈ B i"

using h1 by simp

qed

ultimately show "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

by simp

qed

show "(⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. A i ∩ B i)"

proof

fix x

assume h2 : "x ∈ (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

show "x ∈ (⋂ i ∈ I. A i ∩ B i)"

proof

fix i

assume "i ∈ I"

then have "x ∈ A i"

using h2 by simp

moreover

have "x ∈ B i"

using ‹i ∈ I› h2 by simp

ultimately show "x ∈ A i ∩ B i"

by simp

qed

(* 3ª demostración *)

lemma "(⋂ i ∈ I. A i ∩ B i) = (⋂ i ∈ I. A i) ∩ (⋂ i ∈ I. B i)"

by auto

end

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

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

2. Pares ∪ Impares = Naturales

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

3. Los primos mayores que 2 son impares

1. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

4. s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

5. (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Se puede imprimir o compartir con