Preimage of a Finset under an injective map.

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))

@[simp]

theorem Finset.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α} : x ∈ Finset.preimage s f hf ↔ f x ∈ s

@[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_empty {α : Type u} {β : Type v} {f : α → β} : Finset.preimage ∅ f (_ : ∀ (a : α), a ∈ f ⁻¹' ↑∅ → ∀ (a_2 : α), a_2 ∈ f ⁻¹' ↑∅ → f a = f a_2 → a = a_2) = ∅

@[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 fun x₁ hx₁ x₂ hx₂ => hs x₁ (_ : f x₁ ∈ s) x₂ (_ : f x₂ ∈ s)) = 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 fun x₁ hx₁ x₂ hx₂ => hst x₁ (_ : f x₁ ∈ s ∪ t) x₂ (_ : f x₂ ∈ s ∪ t)) ∪ Finset.preimage t f fun x₁ hx₁ x₂ hx₂ => hst x₁ (_ : f x₁ ∈ s ∪ t) x₂ (_ : f x₂ ∈ s ∪ t)

@[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)))ᶜ

theorem Finset.monotone_preimage {α : Type u} {β : Type v} {f : α → β} (h : Function.Injective f) : Monotone fun s => 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 x, 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.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 : γ), 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 : γ), 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