Image of a Finset α under a partially defined function

In this file we define Part.toFinset and Finset.pimage. We also prove some trivial lemmas about these definitions.

Tags

finite set, image, partial function

def Part.toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] : Finset α

Convert an o : Part α with decidable Part.Dom o to Finset α.

@[simp]

theorem Part.mem_toFinset {α : Type u_1} {o : Part α} [Decidable o.Dom] {x : α} : x ∈ o.toFinset ↔ x ∈ o

@[simp]

theorem Part.toFinset_none {α : Type u_1} [Decidable none.Dom] : none.toFinset = ∅

@[simp]

theorem Part.toFinset_some {α : Type u_1} {a : α} [Decidable (some a).Dom] : (some a).toFinset = {a}

@[simp]

theorem Part.coe_toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] : ↑o.toFinset = {x : α | x ∈ o}

def Finset.pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α →. β) [(x : α) → Decidable (f x).Dom] (s : Finset α) : Finset β

Image of s : Finset α under a partially defined function f : α →. β.

@[simp]

theorem Finset.mem_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {b : β} : b ∈ pimage f s ↔ ∃ a ∈ s, b ∈ f a

@[simp]

theorem Finset.coe_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} : ↑(pimage f s) = f.image ↑s

@[simp]

theorem Finset.pimage_some {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → β) [(x : α) → Decidable (Part.some (f x)).Dom] : pimage (fun (x : α) => Part.some (f x)) s = image f s

theorem Finset.pimage_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f g : α →. β} [(x : α) → Decidable (f x).Dom] [(x : α) → Decidable (g x).Dom] {s t : Finset α} (h₁ : s = t) (h₂ : ∀ x ∈ t, f x = g x) : pimage f s = pimage g t

theorem Finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} : pimage f s = image (fun (x : { x : α // x ∈ {x ∈ s | (f x).Dom} }) => (f ↑x).get ⋯) {x ∈ s | (f x).Dom}.attach

Rewrite s.pimage f in terms of Finset.filter, Finset.attach, and Finset.image.

theorem Finset.pimage_union {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} [DecidableEq α] : pimage f (s ∪ t) = pimage f s ∪ pimage f t

@[simp]

theorem Finset.pimage_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] : pimage f ∅ = ∅

theorem Finset.pimage_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset β} : pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t

theorem Finset.pimage_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} (h : s ⊆ t) : pimage f s ⊆ pimage f t

theorem Finset.pimage_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} [DecidableEq α] : pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t