4 junio 2021 – Calculemus

Unión con intersección general

PorJosé A. Alonso 4 junio 20214 junio 2021

Demostrar que

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

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

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

import data.set.basic
import tactic

open set

variable  {α : Type}
variable  s : set α
variables A : ℕ → set α

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

import data.set.basic

import tactic

open set

variable {α : Type}

variable s : set α

variables A : ℕ → set α

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

sorry

Soluciones