instAlternative — Mathlib

English

The collection of sets carries an Alternative structure with operations defined by singleton, image, union, and empty set, satisfying the standard laws of an Alternative.

Русский

Множества образуют структуру Alternative: единичное множество, отображение образа, объединение и пустое множество, удовлетворяющие стандартным законам альтеративности.

LaTeX

$$$\text{Alternative}(\text{Set})$$$

Lean4

instance : Alternative Set where
  pure a := { a }
  seq s t := s.seq (t ())
  seqLeft s t := {a | a ∈ s ∧ (t ()).Nonempty}
  seqRight s t := {b | s.Nonempty ∧ b ∈ t ()}
  map := Set.image
  orElse s t := s ∪ t ()
  failure := ∅

Похожие утверждения