Demostrar con Lean4 y con Isabelle/HOL que \[ s \setminus (t ∪ u) ⊆ (s \setminus t) \setminus u \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) example : s \ (t ∪ u) ⊆ (s \ t) \ u := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Diferencia_de_diferencia_de_conjuntos_2 imports Main begin lemma "(s - t) - u ⊆ s - (t ∪ u)" oops end
Demostrar con Lean4 y con Isabelle/HOL que \[ (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (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 : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by sorry
y la siguiente teoría de Isabelle/HOL:
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2 imports Main begin lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" oops end
Demostrar con Lean4 y con Isabelle/HOL que \[ (s \setminus t) \setminus u ⊆ s \setminus (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 : (s \ t) \ u ⊆ s \ (t ∪ u) := by sorry
y la la siguiente teoría de Isabelle/HOL:
theory Diferencia_de_diferencia_de_conjuntos imports Main begin lemma "(s - t) - u ⊆ s - (t ∪ u)" oops
Demostrar con Lean4 y con Isabelle/HOL 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
y la siguiente teoría de Isabelle/HOL:
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union imports Main begin lemma "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" oops end
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