19 octubre 2023 – Calculemus

Para cualquier conjunto s, s ⊆ s

PorJosé A. Alonso 19 octubre 202317 octubre 2023

Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

variable {α : Type _}
variable (s : Set α)

example : s ⊆ s :=
by sorry

import Mathlib.Tactic

variable {α : Type _}

variable (s : Set α)

example : s ⊆ s :=

by sorry