L.finish – Calculemus

Pruebas de length (xs ++ ys) = length xs + length ys

PorJosé A. Alonso 9 septiembre 20215 septiembre 2021

En Lean están definidas las funciones

   length : list α → nat
   (++)   : list α → list α → list α

1 2	length : list α → nat (++) : list α → list α → list α

tales que

(length xs) es la longitud de xs. Por ejemplo,

     length [2,3,5,3] = 4

1	length [2,3,5,3] = 4

(xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.

     [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]

1	[1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]

Dichas funciones están caracterizadas por los siguientes lemas:

   length_nil  : length [] = 0
   length_cons : length (x :: xs) = length xs + 1
   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

length_nil : length [] = 0

length_cons : length (x :: xs) = length xs + 1

nil_append : [] ++ ys = ys

cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que

   length (xs ++ ys) = length xs + length ys

1	length (xs ++ ys) = length xs + length ys

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

import tactic
open list

variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)

lemma length_nil  : length ([] : list α) = 0 := rfl

example :
  length (xs ++ ys) = length xs + length ys :=
sorry

import tactic

open list

variable {α : Type}

variable (x : α)

variables (xs ys zs : list α)

lemma length_nil : length ([] : list α) = 0 := rfl

example :

length (xs ++ ys) = length xs + length ys :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open list

variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)

lemma length_nil  : length ([] : list α) = 0 := rfl

-- 1ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    rw add_assoc,
    rw add_comm (length ys),
    rw add_assoc, },
end

-- 2ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- library_search,
    exact add_right_comm (length as) (length ys) 1 },
end

-- 3ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- by hint,
    linarith, },
end

-- 4ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { simp [HI],
    linarith, },
end

-- 5ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { finish [HI],},
end

-- 6ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by induction xs ; finish [*]

-- 7ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : congr_arg length (nil_append ys)
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : congr_arg2 (+) length_nil.symm rfl, },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : congr_arg length (cons_append a as ys)
     ... = length (as ++ ys) + 1        : length_cons a (as ++ ys)
     ... = (length as + length ys) + 1  : congr_arg2 (+) HI rfl
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, },
end

-- 8ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : by rw nil_append
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : by rw length_nil },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : by rw cons_append
     ... = length (as ++ ys) + 1        : by rw length_cons
     ... = (length as + length ys) + 1  : by rw HI
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : by rw length_cons, },
end

-- 9ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( show length ([] ++ ys) = length [] + length ys, from
      calc length ([] ++ ys)
           = length ys                    : by rw nil_append
       ... = 0 + length ys                : by exact (zero_add (length ys)).symm
       ... = length [] + length ys        : by rw length_nil )
  ( assume a as,
    assume HI : length (as ++ ys) = length as + length ys,
    show length ((a :: as) ++ ys) = length (a :: as) + length ys, from
      calc length ((a :: as) ++ ys)
           = length (a :: (as ++ ys))     : by rw cons_append
       ... = length (as ++ ys) + 1        : by rw length_cons
       ... = (length as + length ys) + 1  : by rw HI
       ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
       ... = length (a :: as) + length ys : by rw length_cons)

-- 10ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( by simp)
  ( λ a as HI, by simp [HI, add_right_comm])

-- 11ª demostración
lemma longitud_conc_1 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| [] := by calc
    length ([] ++ ys)
        = length ys                    : by rw nil_append
    ... = 0 + length ys                : by rw zero_add
    ... = length [] + length ys        : by rw length_nil
| (a :: as) := by calc
    length ((a :: as) ++ ys)
        = length (a :: (as ++ ys))     : by rw cons_append
    ... = length (as ++ ys) + 1        : by rw length_cons
    ... = (length as + length ys) + 1  : by rw longitud_conc_1
    ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
    ... = length (a :: as) + length ys : by rw length_cons

-- 12ª demostración
lemma longitud_conc_2 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| []        := by simp
| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]

-- 13ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
-- by library_search
length_append xs ys

-- 14ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by simp

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

import tactic

open list

variable {α : Type}

variable (x : α)

variables (xs ys zs : list α)

lemma length_nil : length ([] : list α) = 0 := rfl

-- 1ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ rw nil_append,

rw length_nil,

rw zero_add, },

{ rw cons_append,

rw length_cons,

rw HI,

rw length_cons,

rw add_assoc,

rw add_comm (length ys),

rw add_assoc, },

end

-- 2ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ rw nil_append,

rw length_nil,

rw zero_add, },

{ rw cons_append,

rw length_cons,

rw HI,

rw length_cons,

-- library_search,

exact add_right_comm (length as) (length ys) 1 },

end

-- 3ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ rw nil_append,

rw length_nil,

rw zero_add, },

{ rw cons_append,

rw length_cons,

rw HI,

rw length_cons,

-- by hint,

linarith, },

end

-- 4ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ simp, },

{ simp [HI],

linarith, },

end

-- 5ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ simp, },

{ finish [HI],},

end

-- 6ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

by induction xs ; finish [*]

-- 7ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ calc length ([] ++ ys)

= length ys : congr_arg length (nil_append ys)

... = 0 + length ys : (zero_add (length ys)).symm

... = length [] + length ys : congr_arg2 (+) length_nil.symm rfl, },

{ calc length ((a :: as) ++ ys)

= length (a :: (as ++ ys)) : congr_arg length (cons_append a as ys)

... = length (as ++ ys) + 1 : length_cons a (as ++ ys)

... = (length as + length ys) + 1 : congr_arg2 (+) HI rfl

... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1

... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, },

end

-- 8ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

begin

induction xs with a as HI,

{ calc length ([] ++ ys)

= length ys : by rw nil_append

... = 0 + length ys : (zero_add (length ys)).symm

... = length [] + length ys : by rw length_nil },

{ calc length ((a :: as) ++ ys)

= length (a :: (as ++ ys)) : by rw cons_append

... = length (as ++ ys) + 1 : by rw length_cons

... = (length as + length ys) + 1 : by rw HI

... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1

... = length (a :: as) + length ys : by rw length_cons, },

end

-- 9ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

list.rec_on xs

( show length ([] ++ ys) = length [] + length ys, from

calc length ([] ++ ys)

= length ys : by rw nil_append

... = 0 + length ys : by exact (zero_add (length ys)).symm

... = length [] + length ys : by rw length_nil )

( assume a as,

assume HI : length (as ++ ys) = length as + length ys,

show length ((a :: as) ++ ys) = length (a :: as) + length ys, from

calc length ((a :: as) ++ ys)

= length (a :: (as ++ ys)) : by rw cons_append

... = length (as ++ ys) + 1 : by rw length_cons

... = (length as + length ys) + 1 : by rw HI

... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1

... = length (a :: as) + length ys : by rw length_cons)

-- 10ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

list.rec_on xs

( by simp)

( λ a as HI, by simp [HI, add_right_comm])

-- 11ª demostración

lemma longitud_conc_1 :

∀ xs, length (xs ++ ys) = length xs + length ys

| [] := by calc

length ([] ++ ys)

= length ys : by rw nil_append

... = 0 + length ys : by rw zero_add

... = length [] + length ys : by rw length_nil

| (a :: as) := by calc

length ((a :: as) ++ ys)

= length (a :: (as ++ ys)) : by rw cons_append

... = length (as ++ ys) + 1 : by rw length_cons

... = (length as + length ys) + 1 : by rw longitud_conc_1

... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1

... = length (a :: as) + length ys : by rw length_cons

-- 12ª demostración

lemma longitud_conc_2 :

∀ xs, length (xs ++ ys) = length xs + length ys

| [] := by simp

| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]

-- 13ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

-- by library_search

length_append xs ys

-- 14ª demostración

example :

length (xs ++ ys) = length xs + length ys :=

by simp

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys"
imports Main
begin

(* 1ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  have "length ([] @ ys) = length ys"
    by (simp only: append_Nil)
  also have "… = 0 + length ys"
    by (rule add_0 [symmetric])
  also have "… = length [] + length ys"
    by (simp only: list.size(3))
  finally show "length ([] @ ys) = length [] + length ys"
    by this
next
  fix x xs
  assume HI : "length (xs @ ys) = length xs + length ys"
  have "length ((x # xs) @ ys) =
        length (x # (xs @ ys))"
    by (simp only: append_Cons)
  also have "… = length (xs @ ys) + 1"
    by (simp only: list.size(4))
  also have "… = (length xs + length ys) + 1"
    by (simp only: HI)
  also have "… = (length xs + 1) + length ys"
    by (simp only: add.assoc add.commute)
  also have "… = length (x # xs) + length ys"
    by (simp only: list.size(4))
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed

(* 2ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  show "length ([] @ ys) = length [] + length ys"
    by simp
next
  fix x xs
  assume "length (xs @ ys) = length xs + length ys"
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed

(* 3ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed

(* 4ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (induct xs) simp_all

(* 5ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (fact length_append)

end

theory "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys"

imports Main

begin

(* 1ª demostración *)

lemma "length (xs @ ys) = length xs + length ys"

proof (induct xs)

have "length ([] @ ys) = length ys"

by (simp only: append_Nil)

also have "… = 0 + length ys"

by (rule add_0 [symmetric])

also have "… = length [] + length ys"

by (simp only: list.size(3))

finally show "length ([] @ ys) = length [] + length ys"

by this

fix x xs

assume HI : "length (xs @ ys) = length xs + length ys"

have "length ((x # xs) @ ys) =

length (x # (xs @ ys))"

by (simp only: append_Cons)

also have "… = length (xs @ ys) + 1"

by (simp only: list.size(4))

also have "… = (length xs + length ys) + 1"

by (simp only: HI)

also have "… = (length xs + 1) + length ys"

by (simp only: add.assoc add.commute)

also have "… = length (x # xs) + length ys"

by (simp only: list.size(4))

then show "length ((x # xs) @ ys) = length (x # xs) + length ys"

by simp

qed

(* 2ª demostración *)

lemma "length (xs @ ys) = length xs + length ys"

proof (induct xs)

show "length ([] @ ys) = length [] + length ys"

by simp

fix x xs

assume "length (xs @ ys) = length xs + length ys"

then show "length ((x # xs) @ ys) = length (x # xs) + length ys"

by simp

qed

(* 3ª demostración *)

lemma "length (xs @ ys) = length xs + length ys"

proof (induct xs)

case Nil

then show ?case by simp

case (Cons a xs)

then show ?case by simp

qed

(* 4ª demostración *)

lemma "length (xs @ ys) = length xs + length ys"

by (induct xs) simp_all

(* 5ª demostración *)

lemma "length (xs @ ys) = length xs + length ys"

by (fact length_append)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las sucesiones divergentes positivas no tienen límites finitos

PorJosé A. Alonso 5 septiembre 20211 septiembre 2021

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

   def limite (u: ℕ → ℝ) (a: ℝ) :=
     ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

1 2	def limite (u: ℕ → ℝ) (a: ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, \|u n - a\| < ε

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

La sucesión u diverge positivamente cuando, para cada número real A, se puede encontrar un número natural m tal que, para n > m , se tenga u(n) > A. En Lean se puede definir por

   def diverge_positivamente (u : ℕ → ℝ) :=
     ∀ A, ∃ m, ∀ n ≥ m, u n > A

1 2	def diverge_positivamente (u : ℕ → ℝ) := ∀ A, ∃ m, ∀ n ≥ m, u n > A

Demostrar que si u diverge positivamente, entonces ningún número real es límite de u.

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

import data.real.basic
import tactic

variable  {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
sorry

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def diverge_positivamente (u : ℕ → ℝ) :=

∀ A, ∃ m, ∀ n ≥ m, u n > A

example

(h : diverge_positivamente u)

: ¬(∃ a, limite u a) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variable  {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

-- 1ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 zero_lt_one with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  specialize hm1 m (le_max_left _ _),
  specialize hm2 m (le_max_right _ _),
  replace hm1 : u m - a < 1 := lt_of_abs_lt hm1,
  replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2,
  apply lt_irrefl (u m),
  calc u m < a + 1 : sub_lt_iff_lt_add'.mp hm1
       ... < u m   : lt_sub_iff_add_lt'.mp hm2,
end

-- 2ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 (by linarith) with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  replace hm1 : |u m - a| < 1 := by finish,
  replace hm1 : u m - a < 1   := lt_of_abs_lt hm1,
  replace hm2 : u m > a + 1   := by finish,
  replace hm2 : 1 < u m - a   := lt_sub_iff_add_lt'.mpr hm2,
  apply lt_irrefl (u m),
  calc u m < a + 1 : by linarith
       ... < u m   : by linarith
end

-- 3ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 (by linarith) with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  specialize hm1 m (le_max_left _ _),
  specialize hm2 m (le_max_right _ _),
  rw abs_lt at hm1,
  linarith,
end

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def diverge_positivamente (u : ℕ → ℝ) :=

∀ A, ∃ m, ∀ n ≥ m, u n > A

-- 1ª demostración

example

(h : diverge_positivamente u)

: ¬(∃ a, limite u a) :=

begin

push_neg,

intros a ha,

cases ha 1 zero_lt_one with m1 hm1,

cases h (a+1) with m2 hm2,

let m := max m1 m2,

specialize hm1 m (le_max_left _ _),

specialize hm2 m (le_max_right _ _),

replace hm1 : u m - a < 1 := lt_of_abs_lt hm1,

replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2,

apply lt_irrefl (u m),

calc u m < a + 1 : sub_lt_iff_lt_add'.mp hm1

... < u m : lt_sub_iff_add_lt'.mp hm2,

end

-- 2ª demostración

example

(h : diverge_positivamente u)

: ¬(∃ a, limite u a) :=

begin

push_neg,

intros a ha,

cases ha 1 (by linarith) with m1 hm1,

cases h (a+1) with m2 hm2,

let m := max m1 m2,

replace hm1 : |u m - a| < 1 := by finish,

replace hm1 : u m - a < 1 := lt_of_abs_lt hm1,

replace hm2 : u m > a + 1 := by finish,

replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2,

apply lt_irrefl (u m),

calc u m < a + 1 : by linarith

... < u m : by linarith

end

-- 3ª demostración

example

(h : diverge_positivamente u)

: ¬(∃ a, limite u a) :=

begin

push_neg,

intros a ha,

cases ha 1 (by linarith) with m1 hm1,

cases h (a+1) with m2 hm2,

let m := max m1 m2,

specialize hm1 m (le_max_left _ _),

specialize hm2 m (le_max_right _ _),

rw abs_lt at hm1,

linarith,

end

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition diverge_positivamente :: "(nat ⇒ real) ⇒ bool"
  where "diverge_positivamente u ⟷ (∀A. ∃m. ∀n≥m. u n > A)"

(* 1ª demostración *)
lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "u ?m < u ?m" using hm1 hm2
  proof -
    have "?m ≥ m1"
      by (rule max.cobounded1)
    have "?m ≥ m2"
      by (rule max.cobounded2)
    have "u ?m - a < 1"
      using hm1 ‹?m ≥ m1› by fastforce
    moreover have "u ?m > a + 1"
      using hm2 ‹?m ≥ m2› by simp
    ultimately show "u ?m < u ?m"
      by simp
  qed
  then show False
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "1 < 1"
  proof -
    have "1 < u ?m - a"
      using hm2
      by (metis add.commute less_diff_eq max.cobounded2)
    also have "… < 1"
      using hm1
      by (metis abs_less_iff max_def order_refl)
    finally show "1 < 1" .
  qed
  then show False
    by auto
qed

end

theory Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition diverge_positivamente :: "(nat ⇒ real) ⇒ bool"

where "diverge_positivamente u ⟷ (∀A. ∃m. ∀n≥m. u n > A)"

(* 1ª demostración *)

lemma

assumes "diverge_positivamente u"

shows "∄a. limite u a"

proof (rule notI)

assume "∃a. limite u a"

then obtain a where "limite u a" try

by auto

then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"

using limite_def by fastforce

obtain m2 where hm2 : "∀n≥m2. u n > a + 1"

using assms diverge_positivamente_def by blast

let ?m = "max m1 m2"

have "u ?m < u ?m" using hm1 hm2

proof -

have "?m ≥ m1"

by (rule max.cobounded1)

have "?m ≥ m2"

by (rule max.cobounded2)

have "u ?m - a < 1"

using hm1 ‹?m ≥ m1› by fastforce

moreover have "u ?m > a + 1"

using hm2 ‹?m ≥ m2› by simp

ultimately show "u ?m < u ?m"

by simp

qed

then show False

by auto

qed

(* 2ª demostración *)

lemma

assumes "diverge_positivamente u"

shows "∄a. limite u a"

proof (rule notI)

assume "∃a. limite u a"

then obtain a where "limite u a" try

by auto

then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"

using limite_def by fastforce

obtain m2 where hm2 : "∀n≥m2. u n > a + 1"

using assms diverge_positivamente_def by blast

let ?m = "max m1 m2"

have "1 < 1"

proof -

have "1 < u ?m - a"

using hm2

by (metis add.commute less_diff_eq max.cobounded2)

also have "… < 1"

using hm1

by (metis abs_less_iff max_def order_refl)

finally show "1 < 1" .

qed

then show False

by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Si a es un punto de acumulación de u, entonces ∀ε>0, ∀ N, ∃k≥N, |u(k)−a| < ε

PorJosé A. Alonso 31 agosto 202125 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

También se puede definir que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean se puede definir por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

1 2	def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

Demostrar que si a es un punto de acumulación de u, entonces

   ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε

1	∀ ε > 0, ∀ N, ∃ k ≥ N, \|u k - a\| < ε

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

import data.real.basic
open nat

variable  {u : ℕ → ℝ}
variables {a : ℝ}
variable  {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=
sorry

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  {u : ℕ → ℝ}
variables {a : ℝ}
variable  {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- En la demostración se usarán los siguientes lemas.

lemma aux1
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

lemma aux2
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
λ N N', ⟨max N N', ⟨le_max_right N N',
                    le_trans (le_max_left N N')
                             (aux1 h (max N N'))⟩⟩

-- 1ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=
begin
  intros ε hε N,
  unfold punto_acumulacion at h,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  unfold limite at hφ2,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  clear hφ1 hφ2,
  use φ m,
  split,
  { exact hm', },
  { exact hN' m hm, },
end

-- 2ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m,
  exact ⟨hm', hN' m hm⟩,
end

-- 3ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end

-- 4ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m ; finish,
end

-- 5ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| < ε,
                  from hN' m hm1,
                show ∃ n ≥ N, |u n - a| < ε,
                  from exists.intro (φ m) (exists.intro hm2 h2)))))

-- 6ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| < ε,
                  from hN' m hm1,
                show ∃ n ≥ N, |u n - a| < ε,
                  from ⟨φ m, hm2, h2⟩))))

-- 7ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| < ε,
                  from hN' m hm1,
                ⟨φ m, hm2, h2⟩))))

-- 8ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                ⟨φ m, hm2, hN' m hm1⟩))))

-- 9ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 10ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from aux2 hφ.1 N N',
        exists.elim h1
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 11ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,
        exists.elim (aux2 hφ.1 N N')
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 12ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      (λ N' hN', exists.elim (aux2 hφ.1 N N')
        (λ m hm, exists.elim hm
          (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 13ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (aux2 hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 14ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
λ ε hε N, exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (aux2 hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- En la demostración se usarán los siguientes lemas.

lemma aux1

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

lemma aux2

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

λ N N', ⟨max N N', ⟨le_max_right N N',

le_trans (le_max_left N N')

(aux1 h (max N N'))⟩⟩

-- 1ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=

begin

intros ε hε N,

unfold punto_acumulacion at h,

rcases h with ⟨φ, hφ1, hφ2⟩,

unfold limite at hφ2,

cases hφ2 ε hε with N' hN',

rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,

clear hφ1 hφ2,

use φ m,

split,

{ exact hm', },

{ exact hN' m hm, },

end

-- 2ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,

use φ m,

exact ⟨hm', hN' m hm⟩,

end

-- 3ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,

exact ⟨φ m, hm', hN' _ hm⟩,

end

-- 4ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,

use φ m ; finish,

end

-- 5ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| < ε,

from hN' m hm1,

show ∃ n ≥ N, |u n - a| < ε,

from exists.intro (φ m) (exists.intro hm2 h2)))))

-- 6ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| < ε,

from hN' m hm1,

show ∃ n ≥ N, |u n - a| < ε,

from ⟨φ m, hm2, h2⟩))))

-- 7ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| < ε,

from hN' m hm1,

⟨φ m, hm2, h2⟩))))

-- 8ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

⟨φ m, hm2, hN' m hm1⟩))))

-- 9ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 10ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

have h1 : ∃ n ≥ N', φ n ≥ N,

from aux2 hφ.1 N N',

exists.elim h1

(λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 11ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε,

exists.elim (aux2 hφ.1 N N')

(λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 12ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (aux2 hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 13ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

(λ φ hφ, exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (aux2 hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 14ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=

λ ε hε N, exists.elim h

(λ φ hφ, exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (aux2 hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos"
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* En la demostración se usarán los siguientes lemas *)
lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed

(* 1ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N"
    using aux2 hφ1 by blast
  have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε"
    using hN' hm1 hm2 by force
  then show "∃k≥N. ¦u k - a¦ < ε"
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed

end

theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos"

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* En la demostración se usarán los siguientes lemas *)

lemma aux1 :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

lemma aux2 :

assumes "extraccion φ"

shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N"

proof (intro allI)

fix N N' :: nat

have "max N N' ≥ N' ∧ φ (max N N') ≥ N"

by (meson assms aux1 max.bounded_iff max.cobounded2)

then show "∃k ≥ N'. φ k ≥ N"

by blast

qed

(* 1ª demostración *)

lemma

assumes "punto_acumulacion u a"

shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix ε :: real and N :: nat

assume "ε > 0"

obtain φ where hφ1 : "extraccion φ"

and hφ2 : "limite (u ∘ φ) a"

using assms punto_acumulacion_def by blast

obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"

using hφ2 limite_def ‹ε > 0› by auto

obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N"

using aux2 hφ1 by blast

have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε"

using hN' hm1 hm2 by force

then show "∃k≥N. ¦u k - a¦ < ε"

by auto

qed

(* 2ª demostración *)

lemma

assumes "punto_acumulacion u a"

shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix ε :: real and N :: nat

assume "ε > 0"

obtain φ where hφ1 : "extraccion φ"

and hφ2 : "limite (u ∘ φ) a"

using assms punto_acumulacion_def by blast

obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"

using hφ2 limite_def ‹ε > 0› by auto

obtain m where "m ≥ N' ∧ φ m ≥ N"

using aux2 hφ1 by blast

then show "∃k≥N. ¦u k - a¦ < ε"

using hN' by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las clases de equivalencia de elementos no relacionados son disjuntas

PorJosé A. Alonso 23 agosto 202121 agosto 2021

Demostrar que las clases de equivalencia de elementos no relacionados son disjuntas.

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

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
sorry

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

-- 1ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  apply hxy,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { contrapose h1,
      intro h1a,
      apply h1a,
      push_neg at h1,
      exact set.eq_empty_iff_forall_not_mem.mpr h1, },
  rcases h2 with ⟨z, hxz, hyz⟩,
  replace hxz : R x z := hxz,
  replace hyz : R y z := hyz,
  have hzy : R z y := hs hyz,
  exact ht hxz hzy,
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { by finish [set.eq_empty_iff_forall_not_mem]},
  apply hxy,
  rcases h2 with ⟨z, hxz, hyz⟩,
  exact ht hxz (hs hyz),
end

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

-- 1ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

apply hxy,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ contrapose h1,

intro h1a,

apply h1a,

push_neg at h1,

exact set.eq_empty_iff_forall_not_mem.mpr h1, },

rcases h2 with ⟨z, hxz, hyz⟩,

replace hxz : R x z := hxz,

replace hyz : R y z := hyz,

have hzy : R z y := hs hyz,

exact ht hxz hzy,

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ by finish [set.eq_empty_iff_forall_not_mem]},

apply hxy,

rcases h2 with ⟨z, hxz, hyz⟩,

exact ht hxz (hs hyz),

end

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas
imports Main
begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"

(* 1ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by (metis CollectD)
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by (metis CollectD)
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by (rule notE)
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 2ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by fastforce
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by fastforce
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by simp
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 3ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis clase_def
            CollectD
            equivp_symp
            equivp_transp
            disjoint_iff)

(* 4ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis equivp_def
            clase_def
            CollectD
            disjoint_iff_not_equal)

end

theory Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas

imports Main

begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"

where "clase R x = {y. R x y}"

(* 1ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by (metis CollectD)

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by (metis CollectD)

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by (rule notE)

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 2ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by fastforce

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by fastforce

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by simp

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 3ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis clase_def

CollectD

equivp_symp

equivp_transp

disjoint_iff)

(* 4ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis equivp_def

clase_def

CollectD

disjoint_iff_not_equal)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición por la izquierda con una inyectiva es una operación inyectiva

PorJosé A. Alonso 20 agosto 202121 agosto 2021

Sean f₁ y f₂ funciones de X en Y y g una función de X en Y. Demostrar que si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂.

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

import tactic

variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}

example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
sorry

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}

-- 1ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  calc g (f₁ x)
       = (g ∘ f₁) x : rfl
   ... = (g ∘ f₂) x : congr_fun hgf x
   ... = g (f₂ x)   : rfl,
end

-- 2ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  exact congr_fun hgf x,
end

-- 3ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  refine funext (λ i, hg _),
  exact congr_fun hgf i,
end

-- 4ª demostración
example
  (hg : function.injective g)
  : function.injective ((∘) g : (X → Y) → (X → Z)) :=
λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : (left_id f₁).symm
    ... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl
    ... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _
    ... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf
    ... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _
    ... = id ∘ f₂              : congr_arg2 (∘) (inv_fun_comp hg) rfl
    ... = f₂                   : left_id f₂

-- 6ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : by finish
    ... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]
    ... = inv_fun g ∘ (g ∘ f₁) : by refl
    ... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]
    ... = (inv_fun g ∘ g) ∘ f₂ : by refl
    ... = id ∘ f₂              : by finish [inv_fun_comp]
    ... = f₂                   : by finish

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

calc g (f₁ x)

= (g ∘ f₁) x : rfl

... = (g ∘ f₂) x : congr_fun hgf x

... = g (f₂ x) : rfl,

end

-- 2ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

exact congr_fun hgf x,

end

-- 3ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

refine funext (λ i, hg _),

exact congr_fun hgf i,

end

-- 4ª demostración

example

(hg : function.injective g)

: function.injective ((∘) g : (X → Y) → (X → Z)) :=

λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : (left_id f₁).symm

... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl

... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _

... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf

... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _

... = id ∘ f₂ : congr_arg2 (∘) (inv_fun_comp hg) rfl

... = f₂ : left_id f₂

-- 6ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : by finish

... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]

... = inv_fun g ∘ (g ∘ f₁) : by refl

... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]

... = (inv_fun g ∘ g) ∘ f₂ : by refl

... = id ∘ f₂ : by finish [inv_fun_comp]

... = f₂ : by finish

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof (rule ext)
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)
  then have "g (f1 x) = g (f2 x)"
    by (simp only: o_apply)
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed

(* 2ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by simp
  then have "g (f1 x) = g (f2 x)"
    by simp
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed

(* 3ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
using assms
by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = id ∘ f1"
    by (rule id_o [symmetric])
  also have "… = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = inv g ∘ (g ∘ f1)"
    by (simp add: comp_assoc)
  also have "… = inv g ∘ (g ∘ f2)"
    using assms(2) by (rule arg_cong)
  also have "… = (inv g ∘ g) ∘ f2"
    by (simp add: comp_assoc)
  also have "… = id ∘ f2"
    by (simp add: assms(1))
  also have "… = f2"
    by (rule id_o)
  finally show "f1 = f2"
    by this
qed

(* 5ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = (inv g ∘ g) ∘ f2"
    using assms(2) by (simp add: comp_assoc)
  also have "… = f2"
    using assms(1) by simp
  finally show "f1 = f2" .
qed

end

theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva

imports Main

begin

(* 1ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof (rule ext)

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)

then have "g (f1 x) = g (f2 x)"

by (simp only: o_apply)

then show "f1 x = f2 x"

using ‹inj g› by (simp only: injD)

qed

(* 2ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by simp

then have "g (f1 x) = g (f2 x)"

by simp

then show "f1 x = f2 x"

using ‹inj g› by (simp only: injD)

qed

(* 3ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

using assms

by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = id ∘ f1"

by (rule id_o [symmetric])

also have "… = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = inv g ∘ (g ∘ f1)"

by (simp add: comp_assoc)

also have "… = inv g ∘ (g ∘ f2)"

using assms(2) by (rule arg_cong)

also have "… = (inv g ∘ g) ∘ f2"

by (simp add: comp_assoc)

also have "… = id ∘ f2"

by (simp add: assms(1))

also have "… = f2"

by (rule id_o)

finally show "f1 = f2"

by this

qed

(* 5ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = (inv g ∘ g) ∘ f2"

using assms(2) by (simp add: comp_assoc)

also have "… = f2"

using assms(1) by simp

finally show "f1 = f2" .

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]