(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)
Demostrar con Lean4 que
\[ (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by sorry |