Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u"
Demostrar con Lean4 e Isabelle/HOL 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
y la siguiente teoría de Isabelle/HOL:
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" oops end