mathlib documentation

data.finset.preimage

Preimage of a finset under an injective map. #

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

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

Equations
@[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
@[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
@[simp]
theorem finset.preimage_empty {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem finset.preimage_univ {α : Type u} {β : Type v} {f : α → β} [fintype α] [fintype β] (hf : set.inj_on f (f ⁻¹' finset.univ)) :
@[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
@[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 _
@[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 _)
theorem finset.monotone_preimage {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) :
monotone (λ (s : finset β), s.preimage f _)
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)) :
theorem finset.map_subset_iff_subset_preimage {α : Type u} {β : Type v} {f : α β} {s : finset α} {t : finset β} :
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
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
theorem finset.preimage_subset {α : Type u} {β : Type v} {f : α β} {s : finset β} {t : finset α} (hs : s finset.map f t) :
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
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
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
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
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)
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)
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 sx set.range fg x = 1) :
(s.preimage f hf).prod (λ (x : α), g (f x)) = s.prod (λ (x : γ), g x)
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 sx set.range fg x = 0) :
(s.preimage f hf).sum (λ (x : α), g (f x)) = s.sum (λ (x : γ), g x)
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)
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)