mathlib3 documentation

data.finset.preimage

Preimage of a finset under an injective map. #

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

source
noncomputable def finset.preimage {α : Type u} {β : Type v} (s : finset β) (f : α → β) (hf : set.inj_on f (f ⁻¹' ↑s)) :
finset α

Preimage of s : finset β under a map f injective of f ⁻¹' s as a finset.

Equations
source
@[simp]
theorem finset.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : finset β} {hf : set.inj_on f (f ⁻¹' ↑s)} {x : α} :
x ∈ s.preimage f hf ↔ f x ∈ s
source
@[simp, norm_cast]
theorem finset.coe_preimage {α : Type u} {β : Type v} {f : α → β} (s : finset β) (hf : set.inj_on f (f ⁻¹' ↑s)) :
↑(s.preimage f hf) = f ⁻¹' ↑s
source
@[simp]
theorem finset.preimage_empty {α : Type u} {β : Type v} {f : α → β} :
∅.preimage f _ = ∅
source
@[simp]
theorem finset.preimage_univ {α : Type u} {β : Type v} {f : α → β} [fintype α] [fintype β] (hf : set.inj_on f (f ⁻¹' ↑finset.univ)) :
finset.univ.preimage f hf = finset.univ
source
@[simp]
theorem finset.preimage_inter {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} {s t : finset β} (hs : set.inj_on f (f ⁻¹' ↑s)) (ht : set.inj_on f (f ⁻¹' ↑t)) :
(s ∩ t).preimage f _ = s.preimage f hs ∩ t.preimage f ht
source
@[simp]
theorem finset.preimage_union {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} {s t : finset β} (hst : set.inj_on f (f ⁻¹' ↑(s ∪ t))) :
(s ∪ t).preimage f hst = s.preimage f _ ∪ t.preimage f _
source
@[simp]
theorem finset.preimage_compl {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] {f : α → β} (s : finset β) (hf : function.injective f) :
sᶜ.preimage f _ = (s.preimage f _)ᶜ
source
@[simp]
theorem finset.preimage_map {α : Type u} {β : Type v} (f : α ↪ β) (s : finset α) :
(finset.map f s).preimage ⇑f _ = s
source
theorem finset.monotone_preimage {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) :
monotone (λ (s : finset β), s.preimage f _)
source
theorem finset.image_subset_iff_subset_preimage {α : Type u} {β : Type v} [decidable_eq β] {f : α → β} {s : finset α} {t : finset β} (hf : set.inj_on f (f ⁻¹' ↑t)) :
finset.image f s ⊆ t ↔ s ⊆ t.preimage f hf
source
theorem finset.map_subset_iff_subset_preimage {α : Type u} {β : Type v} {f : α ↪ β} {s : finset α} {t : finset β} :
finset.map f s ⊆ t ↔ s ⊆ t.preimage ⇑f _
source
theorem finset.image_preimage {α : Type u} {β : Type v} [decidable_eq β] (f : α → β) (s : finset β) [Π (x : β), decidable (x ∈ set.range f)] (hf : set.inj_on f (f ⁻¹' ↑s)) :
finset.image f (s.preimage f hf) = finset.filter (λ (x : β), x ∈ set.range f) s
source
theorem finset.image_preimage_of_bij {α : Type u} {β : Type v} [decidable_eq β] (f : α → β) (s : finset β) (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) :
finset.image f (s.preimage f _) = s
source
theorem finset.preimage_subset {α : Type u} {β : Type v} {f : α ↪ β} {s : finset β} {t : finset α} (hs : s ⊆ finset.map f t) :
s.preimage ⇑f _ ⊆ t
source
theorem finset.subset_map_iff {α : Type u} {β : Type v} {f : α ↪ β} {s : finset β} {t : finset α} :
s ⊆ finset.map f t ↔ ∃ (u : finset α) (H : u ⊆ t), s = finset.map f u
source
theorem finset.sigma_preimage_mk {α : Type u} {β : α → Type u_1} [decidable_eq α] (s : finset (Σ (a : α), β a)) (t : finset α) :
t.sigma (λ (a : α), s.preimage (sigma.mk a) _) = finset.filter (λ (a : Σ (a : α), β a), a.fst ∈ t) s
source
theorem finset.sigma_preimage_mk_of_subset {α : Type u} {β : α → Type u_1} [decidable_eq α] (s : finset (Σ (a : α), β a)) {t : finset α} (ht : finset.image sigma.fst s ⊆ t) :
t.sigma (λ (a : α), s.preimage (sigma.mk a) _) = s
source
theorem finset.sigma_image_fst_preimage_mk {α : Type u} {β : α → Type u_1} [decidable_eq α] (s : finset (Σ (a : α), β a)) :
(finset.image sigma.fst s).sigma (λ (a : α), s.preimage (sigma.mk a) _) = s
source
theorem finset.prod_preimage' {α : Type u} {β : Type v} {γ : Type x} [comm_monoid β] (f : α → γ) [decidable_pred (λ (x : γ), x ∈ set.range f)] (s : finset γ) (hf : set.inj_on f (f ⁻¹' ↑s)) (g : γ → β) :
(s.preimage f hf).prod (λ (x : α), g (f x)) = (finset.filter (λ (x : γ), x ∈ set.range f) s).prod (λ (x : γ), g x)
source
theorem finset.sum_preimage' {α : Type u} {β : Type v} {γ : Type x} [add_comm_monoid β] (f : α → γ) [decidable_pred (λ (x : γ), x ∈ set.range f)] (s : finset γ) (hf : set.inj_on f (f ⁻¹' ↑s)) (g : γ → β) :
(s.preimage f hf).sum (λ (x : α), g (f x)) = (finset.filter (λ (x : γ), x ∈ set.range f) s).sum (λ (x : γ), g x)
source
theorem finset.prod_preimage {α : Type u} {β : Type v} {γ : Type x} [comm_monoid β] (f : α → γ) (s : finset γ) (hf : set.inj_on f (f ⁻¹' ↑s)) (g : γ → β) (hg : ∀ (x : γ), x ∈ s → x ∉ set.range f → g x = 1) :
(s.preimage f hf).prod (λ (x : α), g (f x)) = s.prod (λ (x : γ), g x)
source
theorem finset.sum_preimage {α : Type u} {β : Type v} {γ : Type x} [add_comm_monoid β] (f : α → γ) (s : finset γ) (hf : set.inj_on f (f ⁻¹' ↑s)) (g : γ → β) (hg : ∀ (x : γ), x ∈ s → x ∉ set.range f → g x = 0) :
(s.preimage f hf).sum (λ (x : α), g (f x)) = s.sum (λ (x : γ), g x)
source
theorem finset.sum_preimage_of_bij {α : Type u} {β : Type v} {γ : Type x} [add_comm_monoid β] (f : α → γ) (s : finset γ) (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) (g : γ → β) :
(s.preimage f _).sum (λ (x : α), g (f x)) = s.sum (λ (x : γ), g x)
source
theorem finset.prod_preimage_of_bij {α : Type u} {β : Type v} {γ : Type x} [comm_monoid β] (f : α → γ) (s : finset γ) (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) (g : γ → β) :
(s.preimage f _).prod (λ (x : α), g (f x)) = s.prod (λ (x : γ), g x)