21 febrero 2024 – Calculemus

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

PorJosé A. Alonso 21 febrero 202420 febrero 2024

Demostrar con Lean4 que \(s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)\).

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

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

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s t u : Set α)

example :

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

by sorry