@[simp]
theorem
finset.mem_preimage
{α : Type u}
{β : Type v}
{f : α → β}
{s : finset β}
{hf : set.inj_on f (f ⁻¹' ↑s)}
{x : α} :
@[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
@[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)) :
@[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))) :
@[simp]
theorem
finset.preimage_compl
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
[fintype α]
[fintype β]
{f : α → β}
(s : finset β)
(hf : function.injective 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)) :
finset.image f s ⊆ t ↔ s ⊆ t.preimage f hf
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 α) :
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) :
theorem
finset.sigma_image_fst_preimage_mk
{α : Type u}
{β : α → Type u_1}
[decidable_eq α]
(s : finset (Σ (a : α), β a)) :
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 : γ → β) :
∏ (x : α) in s.preimage f hf, g (f x) = ∏ (x : γ) in finset.filter (λ (x : γ), x ∈ set.range f) s, 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 : γ → β) :
∑ (x : α) in s.preimage f hf, g (f x) = ∑ (x : γ) in finset.filter (λ (x : γ), x ∈ set.range f) s, 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 ∈ s → x ∉ set.range f → g x = 1) :
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) :
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 : γ → β) :
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 : γ → β) :