José A. AlonsoDemostrar que, para cualquier conjunto s, s ⊆ s
Para ello, completar la siguiente teoría de Lean:
import tactic variables {α : Type*} (s : set α) example : s ⊆ s := sorry |
Demostrar que, para cualquier conjunto s, s ⊆ s
Para ello, completar la siguiente teoría de Lean:
import tactic variables {α : Type*} (s : set α) example : s ⊆ s := sorry |