1 junio 2021 – Calculemus

Intersección de los primos y los mayores que dos

PorJosé A. Alonso 1 junio 20211 junio 2021

Los conjuntos de los números primos, los mayores que 2 y los impares se definen por

   def primos      : set ℕ := {n | prime n}
   def mayoresQue2 : set ℕ := {n | n > 2}
   def impares     : set ℕ := {n | ¬ even n}

def primos : set ℕ := {n | prime n}

def mayoresQue2 : set ℕ := {n | n > 2}

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

Demostrar que

   primos ∩ mayoresQue2 ⊆ impares

1	primos ∩ mayoresQue2 ⊆ impares

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

import data.nat.parity
import data.nat.prime
import tactic

open nat

def primos      : set ℕ := {n | prime n}
def mayoresQue2 : set ℕ := {n | n > 2}
def impares     : set ℕ := {n | ¬ even n}

example : primos ∩ mayoresQue2 ⊆ impares :=
sorry

import data.nat.parity

import data.nat.prime

import tactic

open nat

def primos : set ℕ := {n | prime n}

def mayoresQue2 : set ℕ := {n | n > 2}

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

example : primos ∩ mayoresQue2 ⊆ impares :=

sorry

Soluciones