toFinset — Mathlib

English

From an optional value, construct an empty Finset or a singleton Finset depending on whether the option is none or some.

Русский

Из значения типа Option формируется либо пустое множество, либо множество-синглтон в зависимости от того, является ли значение None или Some.

LaTeX

$$$ toFinset (o: Option \alpha) = o.elim \emptyset \{ x \mid x \in o \}$$$

Lean4

/-- Construct an empty or singleton finset from an `Option` -/
def toFinset (o : Option α) : Finset α :=
  o.elim ∅ singleton

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