28 abril 2022 – Calculemus

Distributiva de la intersección respecto de la unión general

PorJosé A. Alonso 28 abril 202228 abril 2022

Demostrar que s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)

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

import data.set.basic
import data.set.lattice
import tactic

open set

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

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

import data.set.basic

import data.set.lattice

import tactic

open set

variable {α : Type}

variable s : set α

variable A : ℕ → set α

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

sorry