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

• s.preimage f hf = ⋯.toFinset

@[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 ⁻¹' ↑univ)) : univ.preimage f hf = univ

@[simp]

theorem Finset.disjoint_preimage {α : Type u} {β : Type v} {f : α → β} {s t : Finset β} {hs : Set.InjOn f (f ⁻¹' ↑s)} {ht : Set.InjOn f (f ⁻¹' ↑t)} (hd : Disjoint s t) : Disjoint (s.preimage f hs) (t.preimage f ht)

@[simp]

theorem Finset.preimage_inter {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} {s 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 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 β) (hfc : Set.InjOn f (f ⁻¹' ↑sᶜ)) (hf : Set.InjOn f (f ⁻¹' ↑s)) : sᶜ.preimage f hfc = (s.preimage f hf)ᶜ

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 α) : (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)) : 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 β} : map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

theorem Finset.card_preimage {α : Type u} {β : Type v} (s : Finset β) (f : α → β) (hf : Set.InjOn f (f ⁻¹' ↑s)) [DecidablePred fun (x : β) => x ∈ Set.range f] : (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card

theorem Finset.image_preimage {α : Type u} {β : Type v} [DecidableEq β] (f : α → β) (s : Finset β) [(x : β) → Decidable (x ∈ Set.range f)] (hf : Set.InjOn f (f ⁻¹' ↑s)) : image f (s.preimage f hf) = {x ∈ s | x ∈ Set.range f}

theorem Finset.image_eq_preimage_of_leftInvOn_injOn {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {g : β → α} {s : Finset α} (hgf : Set.LeftInvOn g f ↑s) (ginj : Set.InjOn g (g ⁻¹' ↑s)) : image f s = s.preimage g ginj

theorem Finset.image_preimage_of_bij {α : Type u} {β : Type v} [DecidableEq β] (f : α → β) (s : Finset β) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : image f (s.preimage f ⋯) = s

theorem Finset.image_preimage_of_bijective {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} (s : Finset β) (hf : Function.Bijective f) : image f (s.preimage f ⋯) = s

theorem Finset.preimage_subset_of_subset_image {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} {s : Finset β} {t : Finset α} (hs : s ⊆ image f t) {hf : Set.InjOn f (f ⁻¹' ↑s)} : s.preimage f hf ⊆ t

theorem Finset.preimage_subset {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s ⊆ map f t) : s.preimage ⇑f ⋯ ⊆ t

theorem Finset.subset_map_iff {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α} : s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

theorem Finset.image_eq_iff_eq_preimage {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} (hf : Function.Bijective f) : image f s = t ↔ s = t.preimage f ⋯

@[simp]

theorem Finset.sup_preimage_self {α : Type u_1} {β : Type u_2} [Nonempty α] [SemilatticeSup β] [OrderBot β] {s : Finset β} {f : α → β} (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : (s.preimage f ⋯).sup f = s.sup id

theorem Finset.sup_preimage_val_id {α : Type u} [Lattice α] [OrderBot α] {P : α → Prop} (Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)) (Pbot : P ⊥) {t : Finset α} (ht : ∀ x ∈ t, P x) : (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩

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) ⋯) = {a ∈ s | a.fst ∈ t}

theorem Finset.sigma_preimage_mk_of_subset {α : Type u} {β : α → Type u_1} [DecidableEq α] (s : Finset ((a : α) × β a)) {t : Finset α} (ht : 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)) : ((image Sigma.fst s).sigma fun (a : α) => s.preimage (Sigma.mk a) ⋯) = s

@[simp]

theorem Finset.preimage_inl {α : Type u} {β : Type v} (s : Finset (α ⊕ β)) : s.preimage Sum.inl ⋯ = s.toLeft

@[simp]

theorem Finset.preimage_inr {α : Type u} {β : Type v} (s : Finset (α ⊕ β)) : s.preimage Sum.inr ⋯ = s.toRight

@[implicit_reducible]

def Equiv.restrictPreimageFinset {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) : ↥(s.preimage ⇑e ⋯) ≃ ↥s

Given an equivalence e : α ≃ β and s : Finset β, restrict e to an equivalence from e ⁻¹' s to s.

Equations

• e.restrictPreimageFinset s = { toFun := fun (a : ↥(s.preimage ⇑e ⋯)) => ⟨e ↑a, ⋯⟩, invFun := fun (b : ↥s) => ⟨e.symm ↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.restrictPreimageFinset_symm_apply_coe {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (b : ↥s) : ↑((e.restrictPreimageFinset s).symm b) = e.symm ↑b

@[simp]

theorem Equiv.restrictPreimageFinset_apply_coe {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (a : ↥(s.preimage ⇑e ⋯)) : ↑((e.restrictPreimageFinset s) a) = e ↑a

theorem Equiv.image_symm_eq_preimage_of_finset {α : Type u} {β : Type v} [DecidableEq α] (e : α ≃ β) (s : Finset β) : Finset.image (⇑e.symm) s = s.preimage ⇑e ⋯

theorem Equiv.image_eq_preimage_symm_of_finset {α : Type u} {β : Type v} [DecidableEq β] (e : α ≃ β) (s : Finset α) : Finset.image (⇑e) s = s.preimage ⇑e.symm ⋯

theorem Finset.restrict_comp_piCongrLeft {α : Type u} {β : Type v} {π : β → Type u_1} (s : Finset β) (e : α ≃ β) : s.restrict ∘ ⇑(Equiv.piCongrLeft π e) = ⇑(Equiv.piCongrLeft (fun (b : ↥s) => π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict

Reindexing and then restricting to a Finset is the same as first restricting to the preimage of this Finset and then reindexing.