enum — Mathlib

English

A Finset s belongs to Finset.enum xs exactly when s is a subset of xs.

Русский

Элемент Finset s принадлежит Finset.enum xs тогда и только тогда, когда s ⊆ xs.

LaTeX

$$$ s \\in \\mathrm{Finset.enum}(xs) \\iff \\forall x \\in s,\\ x \\in xs. $$$

Lean4

/-- enumerate all finite sets of a given type -/
def enum [DecidableEq α] : List α → List (Finset α)
  | [] => [∅]
  | x :: xs => do
    let r ← Finset.enum xs
    [r, insert x r]

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