Documentation

Mathlib.Data.Finset.Preimage

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

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

Equations
  • s.preimage f hf = .toFinset
Instances For
    @[simp]
    theorem Finset.mem_preimage {α : Type u} {β : Type v} {f : αβ} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' s)} {x : α} :
    x s.preimage f hf f x s
    @[simp]
    theorem Finset.coe_preimage {α : Type u} {β : Type v} {f : αβ} (s : Finset β) (hf : Set.InjOn f (f ⁻¹' s)) :
    (s.preimage f hf) = f ⁻¹' s
    @[simp]
    theorem Finset.preimage_empty {α : Type u} {β : Type v} {f : αβ} :
    .preimage f =
    @[simp]
    theorem Finset.preimage_univ {α : Type u} {β : Type v} {f : αβ} [Fintype α] [Fintype β] (hf : Set.InjOn f (f ⁻¹' Finset.univ)) :
    Finset.univ.preimage 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)) :
    (s t).preimage f = s.preimage f hs t.preimage 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))) :
    (s t).preimage f hst = s.preimage f t.preimage f
    @[simp]
    theorem Finset.preimage_compl {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] {f : αβ} (s : Finset β) (hf : Function.Injective f) :
    s.preimage f = (s.preimage f )
    @[simp]
    theorem Finset.preimage_map {α : Type u} {β : Type v} (f : α β) (s : Finset α) :
    (Finset.map f s).preimage f = s
    theorem Finset.monotone_preimage {α : Type u} {β : Type v} {f : αβ} (h : Function.Injective f) :
    Monotone fun (s : Finset β) => s.preimage f
    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 t.preimage f hf
    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
    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 (s.preimage 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 (s.preimage f ) = s
    theorem Finset.preimage_subset {α : Type u} {β : Type v} {f : α β} {s : Finset β} {t : Finset α} (hs : s Finset.map f t) :
    s.preimage f t
    theorem Finset.subset_map_iff {α : Type u} {β : Type v} {f : α β} {s : Finset β} {t : Finset α} :
    s Finset.map f t ut, s = Finset.map f u
    theorem Finset.sigma_preimage_mk {α : Type u} {β : αType u_1} [DecidableEq α] (s : Finset ((a : α) × β a)) (t : Finset α) :
    (t.sigma fun (a : α) => s.preimage (Sigma.mk a) ) = 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) :
    (t.sigma fun (a : α) => s.preimage (Sigma.mk a) ) = s
    theorem Finset.sigma_image_fst_preimage_mk {α : Type u} {β : αType u_1} [DecidableEq α] (s : Finset ((a : α) × β a)) :
    ((Finset.image Sigma.fst s).sigma fun (a : α) => s.preimage (Sigma.mk a) ) = s