2ª propiedad semidistributiva de la intersección sobre la unión
Demostrar que
(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= sorry |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
Read More «2ª propiedad semidistributiva de la intersección sobre la unión»