Tagging a partition of a finite set

Tagging vertices according to a predicate embeds a type into its disjoint sum with itself. The finite-set image formula compares constructions on a single vertex type with constructions on disjoint vertex types.

def TauCeti.partitionEmbedding {α : Type u_1} (p : α → Prop) [DecidablePred p] : α ↪ α ⊕ α

Embed a type into its disjoint sum with itself, tagging elements on the left when they satisfy p and on the right otherwise.

Equations

• TauCeti.partitionEmbedding p = { toFun := fun (x : α) => if p x then Sum.inl x else Sum.inr x, inj' := ⋯ }

@[simp]

theorem TauCeti.partitionEmbedding_apply {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : (partitionEmbedding p) x = if p x then Sum.inl x else Sum.inr x

The partition embedding tags an element according to the predicate.

@[simp]

theorem Finset.image_partitionEmbedding {α : Type u_1} [DecidableEq α] (s : Finset α) (p : α → Prop) [DecidablePred p] : image (⇑(TauCeti.partitionEmbedding p)) s = (filter p s).disjSum ({x ∈ s | ¬p x})

Tagging a finite set according to a predicate gives the disjoint sum of its two parts.