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
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 : α →. β.
Equations
- Finset.pimage f s = s.biUnion fun (x : α) => (f x).toFinset
@[simp]
theorem
Finset.mem_pimage
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
{f : α →. β}
[(x : α) → Decidable (f x).Dom]
{s : Finset α}
{b : β}
:
b ∈ Finset.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 α}
:
↑(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]
:
Finset.pimage (fun (x : α) => Part.some (f x)) s = Finset.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)
:
Finset.pimage f s = Finset.pimage g t
theorem
Finset.pimage_eq_image_filter
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
{f : α →. β}
[(x : α) → Decidable (f x).Dom]
{s : Finset α}
:
Finset.pimage f s = Finset.image (fun (x : { x : α // x ∈ Finset.filter (fun (x : α) => (f x).Dom) s }) => (f ↑x).get ⋯)
(Finset.filter (fun (x : α) => (f x).Dom) s).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 α]
:
Finset.pimage f (s ∪ t) = Finset.pimage f s ∪ Finset.pimage f t
@[simp]
theorem
Finset.pimage_empty
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
{f : α →. β}
[(x : α) → Decidable (f x).Dom]
:
Finset.pimage f ∅ = ∅
theorem
Finset.pimage_subset
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
{f : α →. β}
[(x : α) → Decidable (f x).Dom]
{s : Finset α}
{t : Finset β}
:
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)
:
Finset.pimage f s ⊆ Finset.pimage f t
theorem
Finset.pimage_inter
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
{f : α →. β}
[(x : α) → Decidable (f x).Dom]
{s t : Finset α}
[DecidableEq α]
:
Finset.pimage f (s ∩ t) ⊆ Finset.pimage f s ∩ Finset.pimage f t