Skip to main content

La unión de los pares e impares es el conjunto de los naturales

Conjuntos

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}

Demostrar con Lean4 que

   Pares ∪ Impares = Naturales

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

import Mathlib.Algebra.Ring.Parity

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…

Diferencia de unión e intersección

Conjuntos

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
import Mathlib.Tactic

open Set

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

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

Read more…

Unión con su diferencia

Conjuntos

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 \\setminus t) ∪ t = s ∪ t :=
by sorry

Read more…

Unión con su intersección

Conjuntos

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

Read more…

Conmutatividad de la intersección

Conjuntos

Demostrar con Lean4 que \[ s ∩ t = 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 ∩ t = t ∩ s :=
by sorry

Read more…

Diferencia de diferencia de conjuntos (2)

Conjuntos

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

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

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

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

Read more…

Diferencia de diferencia de conjuntos

Conjuntos

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

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

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

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

Read more…

Propiedad de monotonía de la intersección

Conjuntos

Demostrar con Lean4 que "Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ u\)".

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

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

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
by sorry

Read more…