SetSemiring — Mathlib

English

Correspondence between Set α and SetSemiring α is bijective in the identity sense.

Русский

Соответствие между множеством подмножеств и SetSemiring α является биективным через тождество.

LaTeX

$$$\text{up}: \text{Set } \alpha \cong \text{SetSemiring } \alpha$$$

Lean4

/-- An alias for `Set α`, which has a semiring structure given by `∪` as "addition" and pointwise
  multiplication `*` as "multiplication". -/
def SetSemiring (α : Type*) : Type _ :=
  Set α
deriving Inhabited, PartialOrder, OrderBot

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