Calculemus

Los primos mayores que 2 son impares

PorJosé A. Alonso 6 marzo 20245 marzo 2024

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}

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

1	Primos ∩ MayoresQue2 ⊆ Impares

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

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

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

Pares ∪ Impares = Naturales

PorJosé A. Alonso 5 marzo 20245 marzo 2024

Los conjuntos de los números naturales, de los pares y de los impares se definen en Lean4 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 con Lean4 que

   Pares ∪ Impares = Naturales

1	Pares ∪ Impares = Naturales

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

import Mathlib.Data.Nat.Parity
open Set

def Naturales : Set ℕ := {n | True}
def Pares     : Set ℕ := {n | Even n}
def Impares   : Set ℕ := {n | ¬Even n}

example : Pares ∪ Impares = Naturales :=
by sorry

import Mathlib.Data.Nat.Parity

open Set

def Naturales : Set ℕ := {n | True}

def Pares : Set ℕ := {n | Even n}

def Impares : Set ℕ := {n | ¬Even n}

example : Pares ∪ Impares = Naturales :=

by sorry

Read More «Pares ∪ Impares = Naturales»

(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)

PorJosé A. Alonso 4 marzo 20242 marzo 2024

Demostrar con Lean4 que
\[ (s \setminus t) ∪ (t \setminus s) = (s ∪ t) \setminus (s ∩ t) \]

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

import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

example : (s \\ t) ∪ (t \\ s) = (s ∪ t) \\ (s ∩ t) :=
by sorry

import Mathlib.Data.Set.Basic

open Set

variable {α : Type}

variable (s t : Set α)

example : (s \\ t) ∪ (t \\ s) = (s ∪ t) \\ (s ∩ t) :=

by sorry

(s \ t) ∪ t = s ∪ t

PorJosé A. Alonso 1 marzo 202427 febrero 2024

Demostrar con Lean4 que
\[ (s \setminus t) ∪ t = s ∪ t \]

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

import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

example : (s \ t) ∪ t = s ∪ t :=
by sorry

import Mathlib.Data.Set.Basic

open Set

variable {α : Type}

variable (s t : Set α)

example : (s \ t) ∪ t = s ∪ t :=

by sorry

s ∪ (s ∩ t) = s

PorJosé A. Alonso 29 febrero 202426 febrero 2024

Demostrar con Lean4 que
\[ s ∪ (s ∩ t) = s \]

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

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t : Set α)

example : s ∪ (s ∩ t) = s :=
by sorry

import Mathlib.Data.Set.Basic

open Set

variable {α : Type}

variable (s t : Set α)

example : s ∪ (s ∩ t) = s :=

by sorry