Finset.exists_equiv_extend_of_card_eq
theorem Finset.exists_equiv_extend_of_card_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {t : Finset β},
Fintype.card α = t.card →
∀ {s : Finset α} {f : α → β}, Finset.image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
The theorem `Finset.exists_equiv_extend_of_card_eq` states that for any two types `α` and `β`, where `α` is a finite type and equality in type `β` is decidable, and for any finset `t` of type `β`, if the cardinality of `α` is equal to the cardinality of `t`, then for any finset `s` of `α` and any function `f` from `α` to `β`, if the image of `s` under `f` is a subset of `t` and `f` is injective on `s`, then there exists a function `g` such that for every element `i` in `s`, the value of `g` at `i` is equal to `f(i)`. In other words, any injective function from a finset `s` in a finite type `α` to a finset `t` that has the same cardinality as `α` can be extended to a bijection between `α` and `t`.
More concisely: Given a finite type `α` and decidable equality in type `β`, if the cardinality of `α` equals that of a finset `t` of `β`, and `f` is an injective function from a finset `s` of `α` to `t`, then there exists a bijection `g` from `α` to `t` extending `f`.
|
Set.MapsTo.exists_equiv_extend_of_card_eq
theorem Set.MapsTo.exists_equiv_extend_of_card_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {t : Finset β},
Fintype.card α = t.card →
∀ {s : Set α} {f : α → β}, Set.MapsTo f s ↑t → Set.InjOn f s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
The theorem `Set.MapsTo.exists_equiv_extend_of_card_eq` states that for any two types `α` and `β`, with `α` being a finite type, and any finite set `t` of type `β`, if the number of elements in `α` and `t` are equal, then for any set `s` of type `α` and any function `f` from `α` to `β` that maps `s` to `t` and is injective on `s`, there exists another function `g` such that for every element `i` in `s`, the image of `i` under `g` is equal to the image of `i` under `f`.
In simpler terms, if we have a function that injectively maps some set into another set with the same number of elements, we can extend this function to a bijection between the entire domain and the second set.
More concisely: If `α` is a finite type, `β` is any type, `t` is a finite set of `β`, `s` is a finite set of `α`, `f : α → β` is an injective function from `s` to `t`, then there exists an extension `g : α → β` of `f` that is a bijection.
|
Fintype.card_sum
theorem Fintype.card_sum :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β],
Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
The `Fintype.card_sum` theorem states that for any two types `α` and `β` that are finite (`Fintype`), the cardinality (or the number of elements) of the sum type `α ⊕ β` is equal to the sum of the cardinalities of `α` and `β`. In mathematical terms, if `α` and `β` are finite sets, then the size of the disjoint union of `α` and `β` is equal to the sum of the sizes of `α` and `β`.
More concisely: The cardinality of the sum type `α ⊕ β` in Lean's `Fintype` theory equals the sum of the cardinalities of `α` and `β` for finite types `α` and `β`.
|