Los primos mayores que 2 son impares
Los números primos, los mayores que 2 y los impares se definen en Lean4 por
|
1 2 3 |
def Primos : Set ℕ := {n | Nat.Prime n} def MayoresQue2 : Set ℕ := {n | n > 2} def Impares : Set ℕ := {n | ¬Even n} |
Demostrar con Lean4 que
|
1 |
Primos ∩ MayoresQue2 ⊆ Impares |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Nat.Parity import Mathlib.Data.Nat.Prime import Mathlib.Tactic open Nat def Primos : Set ℕ := {n | Nat.Prime n} def MayoresQue2 : Set ℕ := {n | n > 2} def Impares : Set ℕ := {n | ¬Even n} example : Primos ∩ MayoresQue2 ⊆ Impares := by sorry |