José A. Alonso

s ∪ ⋂ i, A i = ⋂ i, (A i ∪ s)

PorJosé A. Alonso 11 marzo 20248 marzo 2024

Demostrar con Lean4 que
\[ s ∪ ⋂_i A_i = ⋂_i (A_i ∪ s) \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s : Set α)

variable (A : ℕ → Set α)

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

by sorry

⋂ᵢ (Aᵢ ∩ Bᵢ) = (⋂ᵢ Aᵢ) ∩ (⋂ᵢ Bᵢ)

PorJosé A. Alonso 8 marzo 20247 marzo 2024

Demostrar con Lean4 que
\[ ⋂_i (A_i ∩ B_i) = (⋂_i A_i) ∩ (⋂_i B_i) \]

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

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

open Set

variable {α : Type}
variable (A B : ℕ → Set α)

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (A B : ℕ → Set α)

example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=

by sorry

s ∩ (⋃ᵢ Aᵢ) = ⋃ᵢ (Aᵢ ∩ s)

PorJosé A. Alonso 7 marzo 20247 marzo 2024

Demostrar con Lean4 que
\[ s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s) \]

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

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

open Set

variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s : Set α)

variable (A : ℕ → Set α)

example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) :=

by sorry

Read More «s ∩ (⋃ᵢ Aᵢ) = ⋃ᵢ (Aᵢ ∩ s)»

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»