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
@[simp]
theorem
Part.mem_toFinset
{α : Type u_1}
{o : Part α}
[Decidable o.Dom]
{x : α}
:
x ∈ Part.toFinset o ↔ x ∈ o
@[simp]
@[simp]
theorem
Part.toFinset_some
{α : Type u_1}
{a : α}
[Decidable (Part.some a).Dom]
:
Part.toFinset (Part.some a) = {a}
@[simp]
theorem
Part.coe_toFinset
{α : Type u_1}
(o : Part α)
[Decidable o.Dom]
:
↑(Part.toFinset o) = {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 : α →. β.
Equations
- Finset.pimage f s = Finset.biUnion s fun (x : α) => Part.toFinset (f x)
Instances For
@[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) = PFun.image f ↑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 : Finset α}
{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 (_ : (f ↑x).Dom))
(Finset.attach (Finset.filter (fun (x : α) => (f x).Dom) s))
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 : Finset α}
{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 : Finset α}
{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 : Finset α}
{t : Finset α}
[DecidableEq α]
:
Finset.pimage f (s ∩ t) ⊆ Finset.pimage f s ∩ Finset.pimage f t