Mathlib.Data.Finset.Attach

Module docstring

{"# Attaching a proof of membership to a finite set

Main declarations

Finset.attach: Given s : Finset α, attach s forms a finset of elements of the subtype {a // a ∈ s}; in other words, it attaches elements to a proof of membership in the set.

Tags

finite sets, finset

","### attach "}

Finset.attach definition

(s : Finset α) : Finset { x // x ∈ s }

Full source

/-- `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⟩

Finite set with attached membership proofs

Informal description

Given a finite set $ s $ of elements of type $ \alpha $, `Finset.attach s` constructs a new finite set consisting of elements of the subtype $ \{x \mid x \in s\} $, where each element is paired with a proof of its membership in $ s $.

Finset.attach_val theorem

(s : Finset α) : s.attach.1 = s.1.attach

Full source

@[simp]
theorem attach_val (s : Finset α) : s.attach.1 = s.1.attach :=
  rfl

Equality of Attached Multiset Constructions

Informal description

For any finite set $s$ of elements of type $\alpha$, the underlying multiset of the attached set `s.attach` is equal to the attached multiset of the underlying multiset of $s$. That is, the multiset obtained by first attaching membership proofs to the elements of $s$ is the same as attaching membership proofs to the elements of the underlying multiset of $s$.

Finset.mem_attach theorem

(s : Finset α) : ∀ x, x ∈ s.attach

Full source

@[simp]
theorem mem_attach (s : Finset α) : ∀ x, x ∈ s.attach :=
  Multiset.mem_attach _

All Elements in Attached Set Have Membership Proofs

Informal description

For any finite set $s$ of elements of type $\alpha$, every element in the attached set `s.attach` (which consists of pairs of elements and their membership proofs in $s$) is indeed a member of `s.attach`.

Finset.coe_attach theorem

(s : Finset α) : s.attach.toSet = Set.univ

Full source

@[simp, norm_cast]
theorem coe_attach (s : Finset α) : s.attach.toSet = Set.univ := by ext; simp

Universal Property of Attached Finset: $\mathrm{toSet}(\mathrm{attach}(s)) = \mathrm{univ}$

Informal description

For any finite set $s$ of elements of type $\alpha$, the underlying set of the attached finset `s.attach` (consisting of elements paired with their membership proofs in $s$) is equal to the universal set of the subtype $\{x \mid x \in s\}$.