Los primos mayores que 2 son impares
Los números primos, los mayores que 2 y los impares se definen en Lean4 por
def Primos : Set ℕ := {n | Nat.Prime n} def MayoresQue2 : Set ℕ := {n | n > 2} def Impares : Set ℕ := {n | ¬Even n}
Demostrar con Lean4 que
Primos ∩ MayoresQue2 ⊆ Impares
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Ring.Parity 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