20 febrero 2024 – Calculemus

Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u

PorJosé A. Alonso 20 febrero 202420 febrero 2024

Demostrar con Lean4 que «Si \(s ⊆ t\), entonces \(s ∩ u ⊆ t ∩ 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
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s t u : Set α)

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

by sorry