Propiedad de monotonía de la intersección
Demostrar que la intersección es monótona por la izquierda; es decir, si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variable {α : Type} variables s t u : set α example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := sorry |