@[simp]
theorem
Set.bind_def
{α : Type u}
{β : Type u}
{s : Set α}
{f : α → Set β}
:
s >>= f = Set.unionᵢ fun i => Set.unionᵢ fun h => f i
theorem
Set.image2_def
{α : Type u_1}
{β : Type u_1}
{γ : Type u_1}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = Seq.seq (f <$> s) fun x => t
Set.image2
in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.
Equations
- Set.instAlternativeSet = let src := Set.monad; Alternative.mk (fun {α} => ∅) fun {α} s t => s ∪ t ()