Intersección de los primos y los mayores que dos

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

Soluciones con 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 :=
begin
  unfold primos mayoresQue2 impares,
  intro n,
  simp,
  intro hn,
  cases prime.eq_two_or_odd hn with h h,
  { rw h,
    intro,
    linarith, },
  { rw even_iff,
    rw h,
    norm_num },
end

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

begin

unfold primos mayoresQue2 impares,

intro n,

simp,

intro hn,

cases prime.eq_two_or_odd hn with h h,

{ rw h,

intro,

linarith, },

{ rw even_iff,

rw h,

norm_num },

end

Soluciones con Isabelle/HOL

theory Interseccion_de_los_primos_y_los_mayores_que_dos
imports Main "HOL-Number_Theory.Number_Theory"
begin

definition primos :: "nat set" where
  "primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where
  "mayoresQue2 = {n ∈ ℕ . n > 2}"

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

section ‹1ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"
proof
  fix x
  assume "x ∈ primos ∩ mayoresQue2"
  then have "x ∈ ℕ ∧ prime x ∧ 2 < x"
    by (simp add: primos_def mayoresQue2_def)
  then have "x ∈ ℕ ∧ odd x"
    by (simp add: prime_odd_nat)
  then show "x ∈ impares"
    by (simp add: impares_def)
qed

section ‹2ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (simp add: Collect_mono_iff Int_def prime_odd_nat)

section ‹3ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"
  unfolding primos_def mayoresQue2_def impares_def
  by (auto simp add: prime_odd_nat)

end

theory Interseccion_de_los_primos_y_los_mayores_que_dos

imports Main "HOL-Number_Theory.Number_Theory"

begin

definition primos :: "nat set" where

"primos = {n ∈ ℕ . prime n}"

definition mayoresQue2 :: "nat set" where

"mayoresQue2 = {n ∈ ℕ . n > 2}"

definition impares :: "nat set" where

"impares = {n ∈ ℕ . ¬ even n}"

section ‹1ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"

proof

fix x

assume "x ∈ primos ∩ mayoresQue2"

then have "x ∈ ℕ ∧ prime x ∧ 2 < x"

by (simp add: primos_def mayoresQue2_def)

then have "x ∈ ℕ ∧ odd x"

by (simp add: prime_odd_nat)

then show "x ∈ impares"

by (simp add: impares_def)

qed

section ‹2ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (simp add: Collect_mono_iff Int_def prime_odd_nat)

section ‹3ª demostración›

lemma "primos ∩ mayoresQue2 ⊆ impares"

unfolding primos_def mayoresQue2_def impares_def

by (auto simp add: prime_odd_nat)

end

Nuevas soluciones

En los comentarios se pueden escribir nuevas soluciones.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Soluciones

Share this:

Escribe un comentarioCancel reply