Conmutatividad de la intersección
Demostrar que
s ∩ t = t ∩ s
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 = t ∩ s := 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>