Finset.mem_preimage
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
The theorem `Finset.mem_preimage` states that for any types `α` and `β`, a mapping `f` from `α` to `β`, a finite set `s` of type `β`, and given that `f` is injective on the preimage of `s`, for any element `x` of type `α`, `x` is within the preimage of `s` under `f` if and only if `f(x)` is in `s`. In simpler terms, it provides a condition to identify whether an element belongs to the preimage of a set under a certain mapping.
More concisely: Given an injective map `f` from type `α` to type `β`, and a finite set `s` in `β`, an element `x` in `α` is in the preimage of `s` under `f` if and only if `f(x)` is in `s`.
|
Finset.coe_preimage
theorem Finset.coe_preimage :
∀ {α : Type u} {β : Type v} {f : α → β} (s : Finset β) (hf : Set.InjOn f (f ⁻¹' ↑s)),
↑(s.preimage f hf) = f ⁻¹' ↑s
The theorem `Finset.coe_preimage` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any finite set `s` of type `β`, if `f` is injective on the preimage of `s` under `f`, then the preimage of `s` under `f` as a finite set, when coverted back to a set, is equal to the preimage of `s` under `f`. In simple terms, it asserts that the process of creating a finite set from the preimage doesn't change the underlying set, assuming `f` is injective on the preimage of `s`.
More concisely: If `f` is an injective function from `α` to `β`, then the preimage of a finite set `s ∈ β` under `f` equals the set of elements in `α` mapping to `s` under `f`.
|
Finset.image_preimage
theorem Finset.image_preimage :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (f : α → β) (s : Finset β)
[inst_1 : (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
This theorem, named `Finset.image_preimage`, states that for any two types `α` and `β` with decidable equality on `β`, any function `f` from `α` to `β`, and any finite set `s` of `β`, assuming that for any `x` in `β` we can decide if `x` is in the range of `f`, and that `f` is injective on the preimage of `s` under `f`, then the image of the preimage of `s` under `f` is equal to the subset of `s` where each element is in the range of `f`. In other words, it is ensuring that when we take the preimage of a set under a function, and then take the image of that preimage under the same function, we end up with the original set, filtered to only include elements within the range of the function. This theorem is essentially about the interaction between function preimages, images, and set filtering within the context of finite sets.
More concisely: For any injective function from a type with decidable equality to another type with decidable equality, and any finite subset of the range, the image of the preimage under the function is equal to the subset of the range consisting of images of elements in the preimage.
|
Mathlib.Data.Finset.Preimage._auxLemma.1
theorem Mathlib.Data.Finset.Preimage._auxLemma.1 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α},
(x ∈ s.preimage f hf) = (f x ∈ s)
The theorem `Mathlib.Data.Finset.Preimage._auxLemma.1` states that for any types `α` and `β`, a function `f` from `α` to `β`, a `Finset` `s` of type `β`, and a proof `hf` that `f` is injective on the preimage of `s`, and for any element `x` of type `α`, `x` is in the preimage of `s` under `f` if and only if the image of `x` under `f` is in `s`. This theorem essentially relates the membership of an element in the preimage of a set to the membership of its image in the original set.
More concisely: For any injective function `f` from type `α` to type `β`, and `Finset` `s` of type `β`, an element `x` of type `α` is in the preimage of `s` under `f` if and only if `f(x)` is in `s`.
|