Teorema de Cantor

Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.

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

import data.set.basic
open function

variables {α : Type}

example : ∀ f : α → set α, ¬ surjective f :=
sorry

import data.set.basic

open function

variables {α : Type}

example : ∀ f : α → set α, ¬ surjective f :=

sorry

Soluciones con Lean

import data.set.basic
open function

variables {α : Type}

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

example : ∀ f : α → set α, ¬ surjective f :=
begin
  intros f hf,
  let S := {i | i ∉ f i},
  unfold surjective at hf,
  cases hf S with j hj,
  by_cases j ∈ S,
  { dsimp at h,
    apply h,
    rw hj,
    exact h, },
  { apply h,
    rw ← hj at h,
    exact h, },
end

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

example : ∀ f : α → set α, ¬ surjective f :=
begin
  intros f hf,
  let S := {i | i ∉ f i},
  cases hf S with j hj,
  by_cases j ∈ S,
  { apply  h,
    rwa hj, },
  { apply h,
    rwa ← hj at h, },
end

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

example : ∀ f : α → set α, ¬ surjective f :=
begin
  intros f hf,
  let S := {i | i ∉ f i},
  cases hf S with j hj,
  have h : (j ∈ S) = (j ∉ S), from
    calc  (j ∈ S)
        = (j ∉ f j) : set.mem_set_of_eq
    ... = (j ∉ S)   : congr_arg not (congr_arg (has_mem.mem j) hj),
  exact false_of_a_eq_not_a h,
end

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

example : ∀ f : α → set α, ¬ surjective f :=
begin
  intros f hf,
  let S := {i | i ∉ f i},
  cases hf S with j hj,
  have h : (j ∈ S) = (j ∉ S),
  { dsimp,
    exact congr_arg not (congr_arg (has_mem.mem j) hj), },
  { exact false_of_a_eq_not_a (congr_arg not (congr_arg not h)), },
end

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

example : ∀ f : α → set α, ¬ surjective f :=
cantor_surjective

import data.set.basic

open function

variables {α : Type}

-- 1ª demostración

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

example : ∀ f : α → set α, ¬ surjective f :=

begin

intros f hf,

let S := {i | i ∉ f i},

unfold surjective at hf,

cases hf S with j hj,

by_cases j ∈ S,

{ dsimp at h,

apply h,

rw hj,

exact h, },

{ apply h,

rw ← hj at h,

exact h, },

end

-- 2ª demostración

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

example : ∀ f : α → set α, ¬ surjective f :=

begin

intros f hf,

let S := {i | i ∉ f i},

cases hf S with j hj,

by_cases j ∈ S,

{ apply h,

rwa hj, },

{ apply h,

rwa ← hj at h, },

end

-- 3ª demostración

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

example : ∀ f : α → set α, ¬ surjective f :=

begin

intros f hf,

let S := {i | i ∉ f i},

cases hf S with j hj,

have h : (j ∈ S) = (j ∉ S), from

calc (j ∈ S)

= (j ∉ f j) : set.mem_set_of_eq

... = (j ∉ S) : congr_arg not (congr_arg (has_mem.mem j) hj),

exact false_of_a_eq_not_a h,

end

-- 4ª demostración

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

example : ∀ f : α → set α, ¬ surjective f :=

begin

intros f hf,

let S := {i | i ∉ f i},

cases hf S with j hj,

have h : (j ∈ S) = (j ∉ S),

{ dsimp,

exact congr_arg not (congr_arg (has_mem.mem j) hj), },

{ exact false_of_a_eq_not_a (congr_arg not (congr_arg not h)), },

end

-- 5ª demostración

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

example : ∀ f : α → set α, ¬ surjective f :=

cantor_surjective

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

La construcción de las demostraciones se muestra en el siguiente vídeo

Soluciones con Isabelle/HOL

theory Teorema_de_Cantor
imports Main
begin

(* 1ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  show False
  proof (cases "j ∈ ?S")
    assume "j ∈ ?S"
    then have "j ∉ f j"
      by (rule CollectD)
    moreover
    have "j ∈ f j"
      using ‹?S = f j› ‹j ∈ ?S› by (rule subst)
    ultimately show False
      by (rule notE)
  next
    assume "j ∉ ?S"
    with ‹?S = f j› have "j ∉ f j"
      by (rule subst)
    then have "j ∈ ?S"
      by (rule CollectI)
    with ‹j ∉ ?S› show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  have "j ∉ ?S"
  proof (rule notI)
    assume "j ∈ ?S"
    then have "j ∉ f j"
      by (rule CollectD)
    with ‹?S = f j› have "j ∉ ?S"
      by (rule ssubst)
    then show False
      using ‹j ∈ ?S› by (rule notE)
  qed
  moreover
  have "j ∈ ?S"
  proof (rule CollectI)
    show "j ∉ f j"
    proof (rule notI)
      assume "j ∈ f j"
      with ‹?S = f j› have "j ∈ ?S"
        by (rule ssubst)
      then have "j ∉ f j"
        by (rule CollectD)
      then show False
        using ‹j ∈ f j› by (rule notE)
    qed
  qed
  ultimately show False
    by (rule notE)
qed

(* 3ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j" by (rule exE)
  have "j ∉ ?S"
  proof
    assume "j ∈ ?S"
    then have "j ∉ f j" by simp
    with ‹?S = f j› have "j ∉ ?S" by simp
    then show False using ‹j ∈ ?S› by simp
  qed
  moreover
  have "j ∈ ?S"
  proof
    show "j ∉ f j"
    proof
      assume "j ∈ f j"
      with ‹?S = f j› have "j ∈ ?S" by simp
      then have "j ∉ f j" by simp
      then show False using ‹j ∈ f j› by simp
    qed
  qed
  ultimately show False by simp
qed

(* 4ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  have "j ∈ ?S = (j ∉ f j)"
    by (rule mem_Collect_eq)
  also have "… = (j ∉ ?S)"
    by (simp only: ‹?S = f j›)
  finally show False
    by (simp only: simp_thms(10))
qed

(* 5ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j" by (rule exE)
  have "j ∈ ?S = (j ∉ f j)" by simp
  also have "… = (j ∉ ?S)" using ‹?S = f j› by simp
  finally show False by simp
qed

(* 6ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
  unfolding surj_def
  by best

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

theory Teorema_de_Cantor

imports Main

begin

(* 1ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

proof (rule notI)

assume "surj f"

let ?S = "{i. i ∉ f i}"

have "∃ j. ?S = f j"

using ‹surj f› by (simp only: surjD)

then obtain j where "?S = f j"

by (rule exE)

show False

proof (cases "j ∈ ?S")

assume "j ∈ ?S"

then have "j ∉ f j"

by (rule CollectD)

moreover

have "j ∈ f j"

using ‹?S = f j› ‹j ∈ ?S› by (rule subst)

ultimately show False

by (rule notE)

assume "j ∉ ?S"

with ‹?S = f j› have "j ∉ f j"

by (rule subst)

then have "j ∈ ?S"

by (rule CollectI)

with ‹j ∉ ?S› show False

by (rule notE)

qed

(* 2ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

proof (rule notI)

assume "surj f"

let ?S = "{i. i ∉ f i}"

have "∃ j. ?S = f j"

using ‹surj f› by (simp only: surjD)

then obtain j where "?S = f j"

by (rule exE)

have "j ∉ ?S"

proof (rule notI)

assume "j ∈ ?S"

then have "j ∉ f j"

by (rule CollectD)

with ‹?S = f j› have "j ∉ ?S"

by (rule ssubst)

then show False

using ‹j ∈ ?S› by (rule notE)

qed

moreover

have "j ∈ ?S"

proof (rule CollectI)

show "j ∉ f j"

proof (rule notI)

assume "j ∈ f j"

with ‹?S = f j› have "j ∈ ?S"

by (rule ssubst)

then have "j ∉ f j"

by (rule CollectD)

then show False

using ‹j ∈ f j› by (rule notE)

qed

ultimately show False

by (rule notE)

qed

(* 3ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

proof

assume "surj f"

let ?S = "{i. i ∉ f i}"

have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)

then obtain j where "?S = f j" by (rule exE)

have "j ∉ ?S"

proof

assume "j ∈ ?S"

then have "j ∉ f j" by simp

with ‹?S = f j› have "j ∉ ?S" by simp

then show False using ‹j ∈ ?S› by simp

qed

moreover

have "j ∈ ?S"

proof

show "j ∉ f j"

proof

assume "j ∈ f j"

with ‹?S = f j› have "j ∈ ?S" by simp

then have "j ∉ f j" by simp

then show False using ‹j ∈ f j› by simp

qed

ultimately show False by simp

qed

(* 4ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

proof (rule notI)

assume "surj f"

let ?S = "{i. i ∉ f i}"

have "∃ j. ?S = f j"

using ‹surj f› by (simp only: surjD)

then obtain j where "?S = f j"

by (rule exE)

have "j ∈ ?S = (j ∉ f j)"

by (rule mem_Collect_eq)

also have "… = (j ∉ ?S)"

by (simp only: ‹?S = f j›)

finally show False

by (simp only: simp_thms(10))

qed

(* 5ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

proof

assume "surj f"

let ?S = "{i. i ∉ f i}"

have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)

then obtain j where "?S = f j" by (rule exE)

have "j ∈ ?S = (j ∉ f j)" by simp

also have "… = (j ∉ ?S)" using ‹?S = f j› by simp

finally show False by simp

qed

(* 6ª demostración *)

theorem

fixes f :: "'α ⇒ 'α set"

shows "¬ surj f"

unfolding surj_def

by best

end

Share this:

Escribe un comentarioCancel reply