English
The Set functor carries a monadic structure (though not globally, due to lack of computational content).
Русский
Функтор Set имеет монодическую структуру (не глобально из-за отсутствия вычислительного содержания).
LaTeX
$$$\mathrm{Set.monad}$$$
Lean4
/-- The `Set` functor is a monad.
This is not a global instance because it does not have computational content,
so it does not make much sense using `do` notation in general.
Moreover, this would cause monad-related coercions and monad lifting logic to become activated.
Either use `attribute [local instance] Set.monad` to make it be a local instance
or use `SetM.run do ...` when `do` notation is wanted. -/
protected def monad : AlternativeMonad.{u} Set
where
__ : Alternative Set := inferInstance
bind s f := ⋃ i ∈ s, f i
