31 mayo 2021 – Calculemus

Unión de los conjuntos de los pares e impares

PorJosé A. Alonso 31 mayo 202121 agosto 2021

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

   def naturales : set ℕ := {n | true}
   def pares     : set ℕ := {n | even n}
   def impares   : set ℕ := {n | ¬ even n}

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

Demostrar que

   pares ∪ impares = naturales

1	pares ∪ impares = naturales

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

import data.nat.parity
import data.set.basic
import tactic

open set

def naturales : set ℕ := {n | true}
def pares     : set ℕ := {n | even n}
def impares   : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=
sorry

import data.nat.parity

import data.set.basic

import tactic

open set

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=

sorry