Menu Close

Etiqueta: IH.fastforce

Límite de sucesiones no decrecientes

José A. Alonso-

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

En Lean, 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| < ε
<pre lang="text">
donde se usa la notación |x| para el valor absoluto de x
<pre lang="text">
   notation `|`x`|` := abs x

y que la sucesión u es no decreciente por

   def no_decreciente (u : ℕ → ℝ) :=
     ∀ n m, n ≤ m → u n ≤ u m

Demostrar que si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n.

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

import data.real.basic
import tactic
 
variable {u : ℕ → ℝ}
variable (a : ℝ)
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m
 
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic
 
variable {u : ℕ → ℝ}
variable (a : ℝ)
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m
 
-- 1ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  replace H : u n - a > 0 := sub_pos.mpr H,
  cases h (u n - a) H with m hm,
  let k := max n m,
  specialize hm k (le_max_right _ _),
  specialize h' n k (le_max_left _ _),
  replace hm : |u k - a| < u k - a, by
    calc |u k - a| < u n - a : hm
               ... ≤ u k - a : sub_le_sub_right h' a,
  rw ← not_le at hm,
  apply hm,
  exact le_abs_self (u k - a),
end
 
-- 2ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  cases h (u n - a) (by linarith) with m hm,
  specialize hm (max n m) (le_max_right _ _),
  specialize h' n (max n m) (le_max_left _ _),
  rw abs_lt at hm,
  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 Limite_de_sucesiones_no_decrecientes
imports Main HOL.Real
begin
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition no_decreciente :: "(nat ⇒ real) ⇒ bool"
  where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"
 
(* 1ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have "a < u n"
      by (rule not_le_imp_less)
    then have H : "u n - a > 0"
      by (simp only: diff_gt_0_iff_gt)
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "n ≤ ?k"
      by (simp only: assms(2) no_decreciente_def)
    then have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by blast
    have "¦u ?k - a¦ < u n - a"
      by (simp only: hm)
    also have "… ≤ u ?k - a"
      using ‹u n ≤ u ?k› by (rule diff_right_mono)
    finally have "¦u ?k - a¦ < u ?k - a"
      by this
    then have "¬ u ?k - a ≤ ¦u ?k - a¦"
      by (simp only: not_le_imp_less)
    moreover have "u ?k - a ≤ ¦u ?k - a¦"
      by (rule abs_ge_self)
    ultimately show False
      by (rule notE)
  qed
qed
 
(* 2ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have H : "u n - a > 0"
      by simp
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately have "¦u ?k - a¦ < u ?k - a"
      by simp
    then show False
      by simp
  qed
qed
 
(* 3ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by fastforce
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately show False
      by simp
  qed
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]

Soluciones →

Las sucesiones divergentes positivas no tienen límites finitos

José A. Alonso-

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

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

   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

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

[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

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

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]

Soluciones →

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

José A. Alonso-

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

[expand title=»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>
[/expand]

[expand title=»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 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by 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 φ where hφ1 : "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¦"
      using hφ2 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 φ where hφ1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using hφ1 hb limite_subsucesion subsucesion_def by blast
  with hφ2 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>
[/expand]

Soluciones →

Las clases de equivalencia de elementos no relacionados son disjuntas

José A. Alonso-

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

[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

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

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]

Soluciones →