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