21 abril 2022 – Calculemus

Propiedad semidistributiva de la intersección sobre la unión

PorJosé A. Alonso 21 abril 202224 abril 2022

Demostrar que s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u).

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

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

sorry