mathlib3 documentation

data.finset.pimage

Image of a finset α under a partially defined function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define part.to_finset and finset.pimage. We also prove some trivial lemmas about these definitions.

Tags #

finite set, image, partial function

source
def part.to_finset {α : Type u_1} (o : part α) [decidable o.dom] :
finset α

Convert a o : part α with decidable part.dom o to finset α.

Equations
source
@[simp]
theorem part.mem_to_finset {α : Type u_1} {o : part α} [decidable o.dom] {x : α} :
x ∈ o.to_finset ↔ x ∈ o
source
@[simp]
theorem part.to_finset_none {α : Type u_1} [decidable part.none.dom] :
part.none.to_finset = ∅
source
@[simp]
theorem part.to_finset_some {α : Type u_1} {a : α} [decidable (part.some a).dom] :
(part.some a).to_finset = {a}
source
@[simp]
theorem part.coe_to_finset {α : Type u_1} (o : part α) [decidable o.dom] :
↑(o.to_finset) = {x : α | x ∈ o}
source
def finset.pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α →. β) [Π (x : α), decidable (f x).dom] (s : finset α) :
finset β

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

Equations
source
@[simp]
theorem finset.mem_pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} {b : β} :
b ∈ finset.pimage f s ↔ ∃ (a : α) (H : a ∈ s), b ∈ f a
source
@[simp, norm_cast]
theorem finset.coe_pimage {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} :
↑(finset.pimage f s) = f.image ↑s
source
@[simp]
theorem finset.pimage_some {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → β) [Π (x : α), decidable (part.some (f x)).dom] :
finset.pimage (λ (x : α), part.some (f x)) s = finset.image f s
source
theorem finset.pimage_congr {α : Type u_1} {β : Type u_2} [decidable_eq β] {f g : α →. β} [Π (x : α), decidable (f x).dom] [Π (x : α), decidable (g x).dom] {s t : finset α} (h₁ : s = t) (h₂ : ∀ (x : α), x ∈ t → f x = g x) :
finset.pimage f s = finset.pimage g t
source
theorem finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} :
finset.pimage f s = finset.image (λ (x : {x // x ∈ finset.filter (λ (x : α), (f x).dom) s}), (f ↑x).get _) (finset.filter (λ (x : α), (f x).dom) s).attach

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

source
theorem finset.pimage_union {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} [decidable_eq α] :
finset.pimage f (s ∪ t) = finset.pimage f s ∪ finset.pimage f t
source
@[simp]
theorem finset.pimage_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] :
finset.pimage f ∅ = ∅
source
theorem finset.pimage_subset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s : finset α} {t : finset β} :
finset.pimage f s ⊆ t ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ f x → y ∈ t
source
theorem finset.pimage_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} (h : s ⊆ t) :
finset.pimage f s ⊆ finset.pimage f t
source
theorem finset.pimage_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α →. β} [Π (x : α), decidable (f x).dom] {s t : finset α} [decidable_eq α] :
finset.pimage f (s ∩ t) ⊆ finset.pimage f s ∩ finset.pimage f t