Union_de_pares_e_impares.md

Título	Autor
Pares ∪ Impares = Naturales.	José A. Alonso

[mathjax]

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

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

Demostrar con Lean4 que

   Pares ∪ Impares = Naturales

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

import Mathlib.Data.Nat.Parity
open Set

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

example : Pares ∪ Impares = Naturales :=
by sorry

1. Demostración en lenguaje natural

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

2. Demostraciones con Lean4

import Mathlib.Data.Nat.Parity
open Set

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

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

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

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

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

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

3. Demostraciones con Isabelle/HOL

theory Union_de_pares_e_impares
imports Main
begin

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

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

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

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

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

end