Menu Close

Etiqueta: L.rfl

El punto de acumulación de las sucesiones convergente es su límite

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₆, ...

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

que a es un límite de u por

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

que u es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

que a es un punto de acumulación de u por

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

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

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

import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
def convergente (u :   ) :=
   a, limite u a
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
def convergente (u :   ) :=
   a, limite u a
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
-- Lemas auxiliares
-- ================
 
lemma unicidad_limite_aux
  {a b: }
  (ha : limite u a)
  (hb : limite u b)
  : b  a :=
begin
  by_contra h,
  set ε := b - a with hε,
  cases ha (ε/2) (by linarith) with A hA,
  cases hb (ε/2) (by linarith) with B hB,
  set N := max A B with hN,
  have hAN : A  N := le_max_left A B,
  have hBN : B  N := le_max_right A B,
  specialize hA N hAN,
  specialize hB N hBN,
  rw abs_lt at hA hB,
  linarith,
end
 
lemma unicidad_limite
  {a b: }
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (unicidad_limite_aux hb ha)
            (unicidad_limite_aux ha hb)
 
lemma limite_subsucesion_aux
  {φ :   }
  (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 limite_subsucesion
  {φ :   }
  {a : }
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u  φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros k hk,
  calc |(u  φ) k - a|
       = |u (φ k) - a| : rfl
   ... < ε             : hN (φ k) _,
  calc φ k
        k : limite_subsucesion_aux hφ k
   ...  N : hk,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold convergente at hu,
  cases hu with b hb,
  convert hb,
  unfold punto_acumulacion at ha,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  have hφ₃ : limite (u  φ) b,
    from limite_subsucesion hb hφ₁,
  exact unicidad_limite hφ₂ hφ₃,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  apply unicidad_limite hφ₂ _,
  exact limite_subsucesion hb hφ₁,
end
 
-- 2ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),
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>

Soluciones con Isabelle/HOL
theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"
 
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
(* Lemas auxiliares *)
 
lemma unicidad_limite_aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed
 
lemma unicidad_limite :
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1)
    by (rule unicidad_limite_aux)
next
  show "b ≤ a" using assms(1) assms(2)
    by (rule unicidad_limite_aux)
qed
 
lemma limite_subsucesion_aux :
  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 limite_subsucesion :
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: limite_subsucesion_aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed
 
(* Demostración *)
lemma
  assumes "convergente u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof -
  obtain b where hb : "limite u b"
    using assms(1) convergente_def by auto
  obtain φ where1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using1 hb limite_subsucesion subsucesion_def by blast
  with2 have "a = b"
    by (rule unicidad_limite)
  then show "limite u a"
    using hb by simp
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>

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

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

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>

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

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