attach — Mathlib

English

attach s collects the elements of s together with proofs of their membership as a Finset of elements of the subtype.

Русский

attach s объединяет элементы s вместе с доказательствами их принадлежности как множество элементов подтипа.

LaTeX

$$$ \text{attach}(s) = \{ \langle x, hx \rangle : x \in s \}$$$

Lean4

/-- `attach s` takes the elements of `s` and forms a new set of elements of the subtype
`{x // x ∈ s}`. -/
def attach (s : Finset α) : Finset { x // x ∈ s } :=
  ⟨Multiset.attach s.1, nodup_attach.2 s.2⟩

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