eraseNone — Mathlib

English

Given a finite set s of option α, eraseNone s returns the finite set of α consisting of those a for which some a is in s.

Русский

Для конечного множества s из Option α eraseNone s возвращает конечное множество α, состоящее из таких a, что some a ∈ s.

LaTeX

$$$\\text{eraseNone}(s) = \\{a \\in \\alpha \\mid \\text{Some}(a) \\in s\\}$$$

Lean4

/-- Given `s : Finset (Option α)`, `eraseNone s : Finset α` is the set of `x : α` such that
`some x ∈ s`. -/
def eraseNone : Finset (Option α) →o Finset α :=
  (Finset.mapEmbedding (Equiv.optionIsSomeEquiv α).toEmbedding).toOrderHom.comp ⟨Finset.subtype _, subtype_mono⟩

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