noncomputable def
Finset.preimage
{α : Type u}
{β : Type v}
(s : Finset β)
(f : α → β)
(hf : Set.InjOn f (f ⁻¹' ↑s))
:
Finset α
Preimage of s : Finset β under a map f injective on f ⁻¹' s as a Finset.
Equations
- Finset.preimage s f hf = Set.Finite.toFinset (_ : Set.Finite (f ⁻¹' ↑s))
Instances For
@[simp]
theorem
Finset.coe_preimage
{α : Type u}
{β : Type v}
{f : α → β}
(s : Finset β)
(hf : Set.InjOn f (f ⁻¹' ↑s))
:
↑(Finset.preimage s f hf) = f ⁻¹' ↑s
@[simp]
theorem
Finset.preimage_univ
{α : Type u}
{β : Type v}
{f : α → β}
[Fintype α]
[Fintype β]
(hf : Set.InjOn f (f ⁻¹' ↑Finset.univ))
:
Finset.preimage Finset.univ f hf = Finset.univ
@[simp]
theorem
Finset.preimage_inter
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
{s : Finset β}
{t : Finset β}
(hs : Set.InjOn f (f ⁻¹' ↑s))
(ht : Set.InjOn f (f ⁻¹' ↑t))
:
Finset.preimage (s ∩ t) f (_ : ∀ x₁ ∈ f ⁻¹' ↑(s ∩ t), ∀ x₂ ∈ f ⁻¹' ↑(s ∩ t), f x₁ = f x₂ → x₁ = x₂) = Finset.preimage s f hs ∩ Finset.preimage t f ht
@[simp]
theorem
Finset.preimage_union
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
{s : Finset β}
{t : Finset β}
(hst : Set.InjOn f (f ⁻¹' ↑(s ∪ t)))
:
Finset.preimage (s ∪ t) f hst = Finset.preimage s f (_ : ∀ x₁ ∈ f ⁻¹' ↑s, ∀ x₂ ∈ f ⁻¹' ↑s, f x₁ = f x₂ → x₁ = x₂) ∪ Finset.preimage t f (_ : ∀ x₁ ∈ f ⁻¹' ↑t, ∀ x₂ ∈ f ⁻¹' ↑t, f x₁ = f x₂ → x₁ = x₂)
@[simp]
theorem
Finset.preimage_compl
{α : Type u}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
[Fintype α]
[Fintype β]
{f : α → β}
(s : Finset β)
(hf : Function.Injective f)
:
Finset.preimage sᶜ f (_ : Set.InjOn f (f ⁻¹' ↑sᶜ)) = (Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s)))ᶜ
@[simp]
theorem
Finset.preimage_map
{α : Type u}
{β : Type v}
(f : α ↪ β)
(s : Finset α)
:
Finset.preimage (Finset.map f s) ⇑f (_ : Set.InjOn (⇑f) (⇑f ⁻¹' ↑(Finset.map f s))) = s
theorem
Finset.monotone_preimage
{α : Type u}
{β : Type v}
{f : α → β}
(h : Function.Injective f)
:
Monotone fun (s : Finset β) => Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s))
theorem
Finset.image_subset_iff_subset_preimage
{α : Type u}
{β : Type v}
[DecidableEq β]
{f : α → β}
{s : Finset α}
{t : Finset β}
(hf : Set.InjOn f (f ⁻¹' ↑t))
:
Finset.image f s ⊆ t ↔ s ⊆ Finset.preimage t f hf
theorem
Finset.map_subset_iff_subset_preimage
{α : Type u}
{β : Type v}
{f : α ↪ β}
{s : Finset α}
{t : Finset β}
:
Finset.map f s ⊆ t ↔ s ⊆ Finset.preimage t ⇑f (_ : Set.InjOn (⇑f) (⇑f ⁻¹' ↑t))
theorem
Finset.image_preimage
{α : Type u}
{β : Type v}
[DecidableEq β]
(f : α → β)
(s : Finset β)
[(x : β) → Decidable (x ∈ Set.range f)]
(hf : Set.InjOn f (f ⁻¹' ↑s))
:
Finset.image f (Finset.preimage s f hf) = Finset.filter (fun (x : β) => x ∈ Set.range f) s
theorem
Finset.image_preimage_of_bij
{α : Type u}
{β : Type v}
[DecidableEq β]
(f : α → β)
(s : Finset β)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
:
Finset.image f (Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s))) = s
theorem
Finset.preimage_subset
{α : Type u}
{β : Type v}
{f : α ↪ β}
{s : Finset β}
{t : Finset α}
(hs : s ⊆ Finset.map f t)
:
Finset.preimage s ⇑f (_ : Set.InjOn (⇑f) (⇑f ⁻¹' ↑s)) ⊆ t
theorem
Finset.subset_map_iff
{α : Type u}
{β : Type v}
{f : α ↪ β}
{s : Finset β}
{t : Finset α}
:
s ⊆ Finset.map f t ↔ ∃ u ⊆ t, s = Finset.map f u
theorem
Finset.sigma_preimage_mk
{α : Type u}
{β : α → Type u_1}
[DecidableEq α]
(s : Finset ((a : α) × β a))
(t : Finset α)
:
(Finset.sigma t fun (a : α) => Finset.preimage s (Sigma.mk a) (_ : Set.InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = Finset.filter (fun (a : (a : α) × β a) => a.fst ∈ t) s
theorem
Finset.sigma_preimage_mk_of_subset
{α : Type u}
{β : α → Type u_1}
[DecidableEq α]
(s : Finset ((a : α) × β a))
{t : Finset α}
(ht : Finset.image Sigma.fst s ⊆ t)
:
(Finset.sigma t fun (a : α) => Finset.preimage s (Sigma.mk a) (_ : Set.InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = s
theorem
Finset.sigma_image_fst_preimage_mk
{α : Type u}
{β : α → Type u_1}
[DecidableEq α]
(s : Finset ((a : α) × β a))
:
(Finset.sigma (Finset.image Sigma.fst s) fun (a : α) =>
Finset.preimage s (Sigma.mk a) (_ : Set.InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = s
theorem
Finset.sum_preimage'
{α : Type u}
{β : Type v}
{γ : Type x}
[AddCommMonoid β]
(f : α → γ)
[DecidablePred fun (x : γ) => x ∈ Set.range f]
(s : Finset γ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : γ → β)
:
(Finset.sum (Finset.preimage s f hf) fun (x : α) => g (f x)) = Finset.sum (Finset.filter (fun (x : γ) => x ∈ Set.range f) s) fun (x : γ) => g x
theorem
Finset.prod_preimage'
{α : Type u}
{β : Type v}
{γ : Type x}
[CommMonoid β]
(f : α → γ)
[DecidablePred fun (x : γ) => x ∈ Set.range f]
(s : Finset γ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : γ → β)
:
(Finset.prod (Finset.preimage s f hf) fun (x : α) => g (f x)) = Finset.prod (Finset.filter (fun (x : γ) => x ∈ Set.range f) s) fun (x : γ) => g x
theorem
Finset.sum_preimage
{α : Type u}
{β : Type v}
{γ : Type x}
[AddCommMonoid β]
(f : α → γ)
(s : Finset γ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : γ → β)
(hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0)
:
(Finset.sum (Finset.preimage s f hf) fun (x : α) => g (f x)) = Finset.sum s fun (x : γ) => g x
theorem
Finset.prod_preimage
{α : Type u}
{β : Type v}
{γ : Type x}
[CommMonoid β]
(f : α → γ)
(s : Finset γ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : γ → β)
(hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1)
:
(Finset.prod (Finset.preimage s f hf) fun (x : α) => g (f x)) = Finset.prod s fun (x : γ) => g x
theorem
Finset.sum_preimage_of_bij
{α : Type u}
{β : Type v}
{γ : Type x}
[AddCommMonoid β]
(f : α → γ)
(s : Finset γ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : γ → β)
:
(Finset.sum (Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s))) fun (x : α) => g (f x)) = Finset.sum s fun (x : γ) => g x
theorem
Finset.prod_preimage_of_bij
{α : Type u}
{β : Type v}
{γ : Type x}
[CommMonoid β]
(f : α → γ)
(s : Finset γ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : γ → β)
:
(Finset.prod (Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s))) fun (x : α) => g (f x)) = Finset.prod s fun (x : γ) => g x