English
The Finset instance satisfies the laws of an Alternative (and LawfulAlternative): map/functor-like behavior with choice and failure handling, obeying associativity and distributivity with union-like operations.
Русский
Экземпляр Finset удовлетворяет законам Alternative (LawfulAlternative): поведение отображения и выбора с учетом отсутствия элементов, соблюдая ассоциативность и распределение с объединением.
LaTeX
$$$$ \\text{Finset is LawfulAlternative.} $$$$
Lean4
instance : LawfulAlternative Finset where
map_failure _ := Finset.image_empty _
failure_seq _ := Finset.sup_empty
orElse_failure _ := Finset.union_empty _
failure_orElse _ := Finset.empty_union _
orElse_assoc _ _ _ := Finset.union_assoc _ _ _ |>.symm
map_orElse _ _ _ := Finset.image_union _ _
