@[class]
- elems : finset α
- complete : ∀ (x : α), x ∈ fintype.elems α
fintype α means that α is finite, i.e. there are only
finitely many distinct elements of type α. The evidence of this
is a finset elems (a list up to permutation without duplicates),
together with a proof that everything of type α is in the list.
Instances
- unique.fintype
- fin_enum.fintype
- nonempty_fin_lin_ord.to_fintype
- fin.fintype
- empty.fintype
- pempty.fintype
- unit.fintype
- punit.fintype
- bool.fintype
- units_int.fintype
- additive.fintype
- multiplicative.fintype
- units.fintype
- option.fintype
- sigma.fintype
- prod.fintype
- ulift.fintype
- sum.fintype
- list.subtype.fintype
- multiset.subtype.fintype
- finset.subtype.fintype
- finset_coe.fintype
- plift.fintype
- Prop.fintype
- subtype.fintype
- pi.fintype
- d_array.fintype
- array.fintype
- vector.fintype
- quotient.fintype
- finset.fintype
- psigma.fintype
- psigma.fintype_prop_left
- psigma.fintype_prop_right
- psigma.fintype_prop_prop
- set.fintype
- pfun_fintype
- equiv.fintype
- set.fintype_empty
- set.fintype_insert
- set.fintype_singleton
- set.fintype_pure
- set.fintype_univ
- set.fintype_union
- set.fintype_sep
- set.fintype_inter
- set.fintype_image
- set.fintype_range
- set.fintype_map
- set.fintype_Union
- set.fintype_bUnion'
- set.fintype_lt_nat
- set.fintype_le_nat
- set.fintype_prod
- set.fintype_image2
- set.fintype_bind'
- set.fintype_seq
- set.nat.fintype_Iio
- category_theory.discrete_fintype
- category_theory.discrete_hom_fintype
- category_theory.limits.fintype_walking_parallel_pair
- category_theory.limits.fintype
- category_theory.limits.wide_pullback_shape.fintype_obj
- category_theory.limits.wide_pullback_shape.fintype_hom
- category_theory.limits.wide_pushout_shape.fintype_obj
- category_theory.limits.wide_pushout_shape.fintype_hom
- category_theory.limits.fintype_walking_pair
- free_group.fintype
- fintype_bot
- quotient_group.fintype
- matrix.fintype
- quotient_group.quotient.fintype
- composition_as_set_fintype
- composition_fintype
- simple_graph.edges_fintype
- simple_graph.neighbor_set_fintype
- turing.TM2to1.Γ'.fintype
- set.Ico_ℕ_fintype
- set.Ico_pnat_fintype
- set.Ico_ℤ_fintype
- zmod.fintype
- affine.simplex.points_with_circumcenter_index.fintype
- lucas_lehmer.X.fintype
- pgame.fintype_left_moves
- pgame.fintype_right_moves
- pgame.fintype_left_moves_of_aux
- pgame.fintype_right_moves_of_aux
@[simp]
@[instance]
Equations
- finset.order_top = {top := finset.univ _inst_1, le := partial_order.le finset.partial_order, lt := partial_order.lt finset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
Equations
- finset.boolean_algebra = {sup := distrib_lattice.sup finset.distrib_lattice, le := distrib_lattice.le finset.distrib_lattice, lt := distrib_lattice.lt finset.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf finset.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := order_top.top finset.order_top, le_top := _, bot := semilattice_inf_bot.bot finset.semilattice_inf_bot, bot_le := _, compl := λ (s : finset α), finset.univ \ s, sdiff := has_sdiff.sdiff finset.has_sdiff, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}
theorem
finset.compl_eq_univ_sdiff
{α : Type u_1}
[fintype α]
[decidable_eq α]
(s : finset α) :
sᶜ = finset.univ \ s
theorem
finset.eq_univ_iff_forall
{α : Type u_1}
[fintype α]
{s : finset α} :
s = finset.univ ↔ ∀ (x : α), x ∈ s
@[simp]
theorem
finset.univ_inter
{α : Type u_1}
[fintype α]
[decidable_eq α]
(s : finset α) :
finset.univ ∩ s = s
@[simp]
theorem
finset.inter_univ
{α : Type u_1}
[fintype α]
[decidable_eq α]
(s : finset α) :
s ∩ finset.univ = s
@[simp]
theorem
finset.piecewise_univ
{α : Type u_1}
[fintype α]
[Π (i : α), decidable (i ∈ finset.univ)]
{δ : α → Sort u_2}
(f g : Π (i : α), δ i) :
finset.univ.piecewise f g = f
theorem
finset.univ_map_equiv_to_embedding
{α : Type u_1}
{β : Type u_2}
[fintype α]
[fintype β]
(e : α ≃ β) :
@[instance]
def
fintype.decidable_pi_fintype
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), decidable_eq (β a)]
[fintype α] :
decidable_eq (Π (a : α), β a)
Equations
- fintype.decidable_pi_fintype = λ (f g : Π (a : α), β a), decidable_of_iff (∀ (a : α), a ∈ fintype.elems α → f a = g a) _
@[instance]
def
fintype.decidable_forall_fintype
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
[fintype α] :
decidable (∀ (a : α), p a)
Equations
- fintype.decidable_forall_fintype = decidable_of_iff (∀ (a : α), a ∈ finset.univ → p a) fintype.decidable_forall_fintype._proof_1
@[instance]
def
fintype.decidable_exists_fintype
{α : Type u_1}
{p : α → Prop}
[decidable_pred p]
[fintype α] :
decidable (∃ (a : α), p a)
Equations
- fintype.decidable_exists_fintype = decidable_of_iff (∃ (a : α) (H : a ∈ finset.univ), p a) fintype.decidable_exists_fintype._proof_1
@[instance]
def
fintype.decidable_eq_equiv_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
[fintype α] :
decidable_eq (α ≃ β)
Equations
- fintype.decidable_eq_equiv_fintype = λ (a b : α ≃ β), decidable_of_iff (a.to_fun = b.to_fun) _
@[instance]
def
fintype.decidable_injective_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
[fintype α] :
Equations
- fintype.decidable_injective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype
@[instance]
def
fintype.decidable_surjective_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
[fintype α]
[fintype β] :
Equations
- fintype.decidable_surjective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype
@[instance]
def
fintype.decidable_bijective_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
[fintype α]
[fintype β] :
Equations
- fintype.decidable_bijective_fintype = λ (x : α → β), _.mpr and.decidable
@[instance]
def
fintype.decidable_left_inverse_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
(f : α → β)
(g : β → α) :
Equations
- fintype.decidable_left_inverse_fintype f g = show decidable (∀ (x : α), g (f x) = x), from fintype.decidable_forall_fintype
@[instance]
def
fintype.decidable_right_inverse_fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
[fintype β]
(f : α → β)
(g : β → α) :
Equations
- fintype.decidable_right_inverse_fintype f g = show decidable (∀ (x : β), f (g x) = x), from fintype.decidable_forall_fintype
Construct a proof of fintype α from a universal multiset
Construct a proof of fintype α from a universal list
card α is the number of elements in α, defined when α is a fintype.
Equations
If l lists all the elements of α without duplicates, then α ≃ fin (l.length).
def
fintype.equiv_fin
(α : Type u_1)
[decidable_eq α]
[fintype α] :
trunc (α ≃ fin (fintype.card α))
There is (computably) a bijection between α and fin n where
n = card α. Since it is not unique, and depends on which permutation
of the universe list is used, the bijection is wrapped in trunc to
preserve computability.
Equations
- fintype.equiv_fin α = _.mpr (quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), x ∈ l) (nd : l.nodup), trunc.mk (fintype.equiv_fin_of_forall_mem_list h nd)) finset.mem_univ_val _)
@[instance]
Equations
- fintype.subtype s H = {elems := {val := multiset.pmap subtype.mk s.val _, nodup := _}, complete := _}
theorem
fintype.subtype_card
{α : Type u_1}
{p : α → Prop}
(s : finset α)
(H : ∀ (x : α), x ∈ s ↔ p x) :
fintype.card {x // p x} = s.card
theorem
fintype.card_of_subtype
{α : Type u_1}
{p : α → Prop}
(s : finset α)
(H : ∀ (x : α), x ∈ s ↔ p x)
[fintype {x // p x}] :
fintype.card {x // p x} = s.card
Construct a fintype from a finset with the same elements.
Equations
- fintype.of_finset s H = fintype.subtype s H
def
fintype.of_bijective
{α : Type u_1}
{β : Type u_2}
[fintype α]
(f : α → β) :
function.bijective f → fintype β
If f : α → β is a bijection and α is a fintype, then β is also a fintype.
Equations
- fintype.of_bijective f H = {elems := finset.map {to_fun := f, inj' := _} finset.univ, complete := _}
def
fintype.of_surjective
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
[fintype α]
(f : α → β) :
function.surjective f → fintype β
If f : α → β is a surjection and α is a fintype, then β is also a fintype.
Equations
- fintype.of_surjective f H = {elems := finset.image f finset.univ, complete := _}
def
fintype.of_injective
{α : Type u_1}
{β : Type u_2}
[fintype β]
(f : α → β) :
function.injective f → fintype α
Equations
- fintype.of_injective f H = let _inst : Π (p : Prop), decidable p := classical.dec in dite (nonempty α) (λ (hα : nonempty α), let _inst_2 : inhabited α := classical.inhabited_of_nonempty hα in fintype.of_surjective (function.inv_fun f) _) (λ (hα : ¬nonempty α), {elems := ∅, complete := _})
If f : α ≃ β and α is a fintype, then β is also a fintype.
Equations
- fintype.of_equiv α f = fintype.of_bijective ⇑f _
theorem
fintype.card_congr
{α : Type u_1}
{β : Type u_2}
[fintype α]
[fintype β] :
α ≃ β → fintype.card α = fintype.card β
theorem
fintype.card_eq
{α : Type u_1}
{β : Type u_2}
[F : fintype α]
[G : fintype β] :
fintype.card α = fintype.card β ↔ nonempty (α ≃ β)
Equations
- fintype.of_subsingleton a = {elems := {a}, complete := _}
@[simp]
@[simp]
Construct a finset enumerating a set s, given a fintype instance.
Equations
- s.to_finset = {val := multiset.map subtype.val finset.univ.val, nodup := _}
@[simp]
theorem
set.to_finset_card
{α : Type u_1}
(s : set α)
[fintype ↥s] :
s.to_finset.card = fintype.card ↥s
theorem
finset.card_univ_diff
{α : Type u_1}
[decidable_eq α]
[fintype α]
(s : finset α) :
(finset.univ \ s).card = fintype.card α - s.card
@[instance]
Equations
- fin.fintype n = {elems := finset.fin_range n, complete := _}
@[instance]
Equations
@[simp]
@[instance]
@[instance]
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
- units_int.fintype = {elems := {1, -1}, complete := units_int.fintype._proof_1}
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
Equations
- s.insert_none = {val := option.none :: multiset.map option.some s.val, nodup := _}
@[simp]
theorem
finset.mem_insert_none
{α : Type u_1}
{s : finset α}
{o : option α} :
o ∈ s.insert_none ↔ ∀ (a : α), a ∈ o → a ∈ s
theorem
finset.some_mem_insert_none
{α : Type u_1}
{s : finset α}
{a : α} :
option.some a ∈ s.insert_none ↔ a ∈ s
@[instance]
Equations
- option.fintype = {elems := finset.univ.insert_none, complete := _}
@[simp]
theorem
fintype.card_option
{α : Type u_1}
[fintype α] :
fintype.card (option α) = fintype.card α + 1
@[instance]
Equations
- sigma.fintype β = {elems := finset.univ.sigma (λ (_x : α), finset.univ), complete := _}
@[simp]
theorem
finset.univ_sigma_univ
{α : Type u_1}
{β : α → Type u_2}
[fintype α]
[Π (a : α), fintype (β a)] :
finset.univ.sigma (λ (a : α), finset.univ) = finset.univ
@[instance]
Equations
- prod.fintype α β = {elems := finset.univ.product finset.univ, complete := _}
@[simp]
theorem
fintype.card_prod
(α : Type u_1)
(β : Type u_2)
[fintype α]
[fintype β] :
fintype.card (α × β) = fintype.card α * fintype.card β
def
fintype.fintype_prod_left
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype (α × β)]
[nonempty β] :
fintype α
Equations
- fintype.fintype_prod_left = {elems := finset.image prod.fst (fintype.elems (α × β)), complete := _}
def
fintype.fintype_prod_right
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
[fintype (α × β)]
[nonempty α] :
fintype β
Equations
- fintype.fintype_prod_right = {elems := finset.image prod.snd (fintype.elems (α × β)), complete := _}
@[instance]
Equations
@[simp]
@[instance]
Equations
- sum.fintype α β = fintype.of_equiv (Σ (b : bool), cond b (ulift α) (ulift β)) ((equiv.sum_equiv_sigma_bool (ulift α) (ulift β)).symm.trans (equiv.ulift.sum_congr equiv.ulift))
theorem
fintype.card_le_of_injective
{α : Type u_1}
{β : Type u_2}
[fintype α]
[fintype β]
(f : α → β) :
function.injective f → fintype.card α ≤ fintype.card β
theorem
fintype.card_eq_one_iff
{α : Type u_1}
[fintype α] :
fintype.card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x
def
fintype.card_eq_zero_equiv_equiv_pempty
{α : Type v}
[fintype α] :
fintype.card α = 0 ≃ (α ≃ pempty)
A fintype with cardinality zero is (constructively) equivalent to pempty.
theorem
fintype.card_le_one_iff
{α : Type u_1}
[fintype α] :
fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b
theorem
fintype.card_le_one_iff_subsingleton
{α : Type u_1}
[fintype α] :
fintype.card α ≤ 1 ↔ subsingleton α
theorem
fintype.one_lt_card_iff_nontrivial
{α : Type u_1}
[fintype α] :
1 < fintype.card α ↔ nontrivial α
theorem
fintype.exists_ne_of_one_lt_card
{α : Type u_1}
[fintype α]
(h : 1 < fintype.card α)
(a : α) :
∃ (b : α), b ≠ a
theorem
fintype.exists_pair_of_one_lt_card
{α : Type u_1}
[fintype α] :
1 < fintype.card α → (∃ (a b : α), a ≠ b)
theorem
fintype.injective_iff_surjective_of_equiv
{α : Type u_1}
{β : Type u_2}
[fintype α]
{f : α → β} :
α ≃ β → (function.injective f ↔ function.surjective f)
theorem
fintype.coe_image_univ
{α : Type u_1}
{β : Type u_2}
[fintype α]
[decidable_eq β]
{f : α → β} :
↑(finset.image f finset.univ) = set.range f
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
A finset of a subsingleton type has cardinality at most one.
@[instance]
def
subtype.fintype
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
[fintype α] :
fintype {x // p x}
Equations
Equations
- set_fintype s = subtype.fintype (λ (x : α), x ∈ s)
An embedding from a fintype to itself can be promoted to an equivalence.
Equations
@[simp]
theorem
function.embedding.equiv_of_fintype_self_embedding_to_embedding
{α : Type u_1}
[fintype α]
(e : α ↪ α) :
@[simp]
Given for all a : α a finset t a of δ a, then one can define the
finset fintype.pi_finset t of all functions taking values in t a for all a. This is the
analogue of finset.pi where the base finset is univ (but formally they are not the same, as
there is an additional condition i ∈ finset.univ in the finset.pi definition).
Equations
- fintype.pi_finset t = finset.map {to_fun := λ (f : Π (a : α), a ∈ finset.univ → δ a) (a : α), f a _, inj' := _} (finset.univ.pi t)
@[simp]
theorem
fintype.mem_pi_finset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_4}
{t : Π (a : α), finset (δ a)}
{f : Π (a : α), δ a} :
f ∈ fintype.pi_finset t ↔ ∀ (a : α), f a ∈ t a
theorem
fintype.pi_finset_subset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_4}
(t₁ t₂ : Π (a : α), finset (δ a)) :
(∀ (a : α), t₁ a ⊆ t₂ a) → fintype.pi_finset t₁ ⊆ fintype.pi_finset t₂
theorem
fintype.pi_finset_disjoint_of_disjoint
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_4}
[Π (a : α), decidable_eq (δ a)]
(t₁ t₂ : Π (a : α), finset (δ a))
{a : α} :
disjoint (t₁ a) (t₂ a) → disjoint (fintype.pi_finset t₁) (fintype.pi_finset t₂)
pi
@[instance]
def
pi.fintype
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
[fintype α]
[Π (a : α), fintype (β a)] :
fintype (Π (a : α), β a)
A dependent product of fintypes, indexed by a fintype, is a fintype.
Equations
- pi.fintype = {elems := fintype.pi_finset (λ (_x : α), finset.univ), complete := _}
@[simp]
theorem
fintype.pi_finset_univ
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
[fintype α]
[Π (a : α), fintype (β a)] :
fintype.pi_finset (λ (a : α), finset.univ) = finset.univ
@[instance]
Equations
- d_array.fintype = fintype.of_equiv (Π (i : fin n), α i) (equiv.d_array_equiv_fin α).symm
@[instance]
Equations
@[instance]
Equations
- vector.fintype = fintype.of_equiv (fin n → α) (equiv.vector_equiv_fin α n).symm
@[instance]
Equations
@[instance]
Equations
- finset.fintype = {elems := finset.univ.powerset, complete := _}
@[simp]
theorem
fintype.card_finset
{α : Type u_1}
[fintype α] :
fintype.card (finset α) = 2 ^ fintype.card α
@[simp]
theorem
fintype.card_subtype_le
{α : Type u_1}
[fintype α]
(p : α → Prop)
[decidable_pred p] :
fintype.card {x // p x} ≤ fintype.card α
theorem
fintype.card_subtype_lt
{α : Type u_1}
[fintype α]
{p : α → Prop}
[decidable_pred p]
{x : α} :
¬p x → fintype.card {x // p x} < fintype.card α
@[instance]
def
psigma.fintype
{α : Type u_1}
{β : α → Type u_2}
[fintype α]
[Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
- psigma.fintype = fintype.of_equiv (Σ (i : α), β i) (equiv.psigma_equiv_sigma (λ (a : α), β a)).symm
@[instance]
def
psigma.fintype_prop_left
{α : Prop}
{β : α → Type u_1}
[decidable α]
[Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
@[instance]
def
psigma.fintype_prop_right
{α : Type u_1}
{β : α → Prop}
[Π (a : α), decidable (β a)]
[fintype α] :
fintype (Σ' (a : α), β a)
Equations
- psigma.fintype_prop_right = fintype.of_equiv {a // β a} {to_fun := λ (_x : {a // β a}), psigma.fintype_prop_right._match_1 _x, inv_fun := λ (_x : Σ' (a : α), β a), psigma.fintype_prop_right._match_2 _x, left_inv := _, right_inv := _}
- psigma.fintype_prop_right._match_1 ⟨x, y⟩ = ⟨x, y⟩
- psigma.fintype_prop_right._match_2 ⟨x, y⟩ = ⟨x, y⟩
@[instance]
def
psigma.fintype_prop_prop
{α : Prop}
{β : α → Prop}
[decidable α]
[Π (a : α), decidable (β a)] :
fintype (Σ' (a : α), β a)
@[instance]
Equations
- set.fintype = {elems := finset.map {to_fun := coe lift_base, inj' := _} finset.univ.powerset, complete := _}
@[instance]
def
pfun_fintype
(p : Prop)
[decidable p]
(α : p → Type u_1)
[Π (hp : p), fintype (α hp)] :
fintype (Π (hp : p), α hp)
theorem
mem_image_univ_iff_mem_range
{α : Type u_1}
{β : Type u_2}
[fintype α]
[decidable_eq β]
{f : α → β}
{b : β} :
b ∈ finset.image f finset.univ ↔ b ∈ set.range f
theorem
card_lt_card_of_injective_of_not_mem
{α : Type u_1}
{β : Type u_2}
[fintype α]
[fintype β]
(f : α → β)
(h : function.injective f)
{b : β} :
b ∉ set.range f → fintype.card α < fintype.card β
def
quotient.fin_choice_aux
{ι : Type u_1}
[decidable_eq ι]
{α : ι → Type u_2}
[S : Π (i : ι), setoid (α i)]
(l : list ι) :
Equations
- quotient.fin_choice_aux (i :: l) f = (f i _).lift_on₂ (quotient.fin_choice_aux l (λ (j : ι) (h : j ∈ l), f j _)) (λ (a : α i) (l_1 : Π (i : ι), i ∈ l → α i), ⟦(λ (j : ι) (h : j ∈ i :: l), dite (j = i) (λ (e : j = i), _.mpr a) (λ (e : ¬j = i), l_1 j _))⟧) _
- quotient.fin_choice_aux list.nil f = ⟦(λ (i : ι), false.elim)⟧
theorem
quotient.fin_choice_aux_eq
{ι : Type u_1}
[decidable_eq ι]
{α : ι → Type u_2}
[S : Π (i : ι), setoid (α i)]
(l : list ι)
(f : Π (i : ι), i ∈ l → α i) :
def
quotient.fin_choice
{ι : Type u_1}
[decidable_eq ι]
[fintype ι]
{α : ι → Type u_2}
[S : Π (i : ι), setoid (α i)] :
Equations
- quotient.fin_choice f = quotient.lift_on (quotient.rec_on finset.univ.val (λ (l : list ι), quotient.fin_choice_aux l (λ (i : ι) (_x : i ∈ l), f i)) _) (λ (f : Π (i : ι), i ∈ finset.univ.val → α i), ⟦(λ (i : ι), f i _)⟧) quotient.fin_choice._proof_2
theorem
quotient.fin_choice_eq
{ι : Type u_1}
[decidable_eq ι]
[fintype ι]
{α : ι → Type u_2}
[Π (i : ι), setoid (α i)]
(f : Π (i : ι), α i) :
Equations
- perms_of_list (a :: l) = perms_of_list l ++ l.bind (λ (b : α), list.map (λ (f : equiv.perm α), equiv.swap a b * f) (perms_of_list l))
- perms_of_list list.nil = [1]
theorem
length_perms_of_list
{α : Type u_1}
[decidable_eq α]
(l : list α) :
(perms_of_list l).length = l.length.fact
theorem
mem_perms_of_list_of_mem
{α : Type u_1}
[decidable_eq α]
{l : list α}
{f : equiv.perm α} :
(∀ (x : α), ⇑f x ≠ x → x ∈ l) → f ∈ perms_of_list l
theorem
mem_of_mem_perms_of_list
{α : Type u_1}
[decidable_eq α]
{l : list α}
{f : equiv.perm α}
(a : f ∈ perms_of_list l)
{x : α} :
theorem
nodup_perms_of_list
{α : Type u_1}
[decidable_eq α]
{l : list α} :
l.nodup → (perms_of_list l).nodup
Equations
- perms_of_finset s = quotient.hrec_on s.val (λ (l : list α) (hl : multiset.nodup ⟦l⟧), {val := ↑(perms_of_list l), nodup := _}) perms_of_finset._proof_2 _
theorem
card_perms_of_finset
{α : Type u_1}
[decidable_eq α]
(s : finset α) :
(perms_of_finset s).card = s.card.fact
Equations
- fintype_perm = {elems := perms_of_finset finset.univ, complete := _}
@[instance]
def
equiv.fintype
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
[fintype α]
[fintype β] :
Equations
- equiv.fintype = dite (fintype.card β = fintype.card α) (λ (h : fintype.card β = fintype.card α), (fintype.equiv_fin α).rec_on_subsingleton (λ (eα : α ≃ fin (fintype.card α)), (fintype.equiv_fin β).rec_on_subsingleton (λ (eβ : β ≃ fin (fintype.card β)), fintype.of_equiv (equiv.perm α) ((equiv.refl α).equiv_congr (eα.trans (h.rec_on eβ.symm)))))) (λ (h : ¬fintype.card β = fintype.card α), {elems := ∅, complete := _})
theorem
fintype.card_perm
{α : Type u_1}
[decidable_eq α]
[fintype α] :
fintype.card (equiv.perm α) = (fintype.card α).fact
theorem
fintype.card_equiv
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
[fintype α]
[fintype β] :
α ≃ β → fintype.card (α ≃ β) = (fintype.card α).fact
theorem
univ_eq_singleton_of_card_one
{α : Type u_1}
[fintype α]
(x : α) :
fintype.card α = 1 → finset.univ = {x}
def
fintype.choose_x
{α : Type u_1}
[decidable_eq α]
[fintype α]
(p : α → Prop)
[decidable_pred p] :
(∃! (a : α), p a) → {a // p a}
Equations
- fintype.choose_x p hp = ⟨finset.choose p finset.univ _, _⟩
def
fintype.choose
{α : Type u_1}
[decidable_eq α]
[fintype α]
(p : α → Prop)
[decidable_pred p] :
(∃! (a : α), p a) → α
Equations
- fintype.choose p hp = ↑(fintype.choose_x p hp)
theorem
fintype.choose_spec
{α : Type u_1}
[decidable_eq α]
[fintype α]
(p : α → Prop)
[decidable_pred p]
(hp : ∃! (a : α), p a) :
p (fintype.choose p hp)
def
fintype.bij_inv
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
[decidable_eq β]
[fintype β]
{f : α → β} :
function.bijective f → β → α
bij_inv fis the unique inverse to a bijectionf. This acts
as a computable alternative tofunction.inv_fun`.
Equations
- fintype.bij_inv f_bij b = fintype.choose (λ (a : α), f a = b) _
theorem
fintype.left_inverse_bij_inv
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
[decidable_eq β]
[fintype β]
{f : α → β}
(f_bij : function.bijective f) :
function.left_inverse (fintype.bij_inv f_bij) f
theorem
fintype.right_inverse_bij_inv
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
[decidable_eq β]
[fintype β]
{f : α → β}
(f_bij : function.bijective f) :
function.right_inverse (fintype.bij_inv f_bij) f
theorem
fintype.bijective_bij_inv
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[fintype α]
[decidable_eq β]
[fintype β]
{f : α → β}
(f_bij : function.bijective f) :
function.bijective (fintype.bij_inv f_bij)
theorem
fintype.well_founded_of_trans_of_irrefl
{α : Type u_1}
[fintype α]
(r : α → α → Prop)
[is_trans α r]
[is_irrefl α r] :
@[instance]
@[class]
Instances
theorem
infinite.exists_not_mem_finset
{α : Type u_1}
[infinite α]
(s : finset α) :
∃ (x : α), x ∉ s
theorem
infinite.of_injective
{α : Type u_1}
{β : Type u_2}
[infinite β]
(f : β → α) :
function.injective f → infinite α
theorem
infinite.of_surjective
{α : Type u_1}
{β : Type u_2}
[infinite β]
(f : α → β) :
function.surjective f → infinite α
Embedding of ℕ into an infinite type.
Equations
- infinite.nat_embedding α = {to_fun := nat_embedding_aux α _inst_1, inj' := _}
theorem
not_injective_infinite_fintype
{α : Type u_1}
{β : Type u_2}
[infinite α]
[fintype β]
(f : α → β) :
theorem
not_surjective_fintype_infinite
{α : Type u_1}
{β : Type u_2}
[fintype α]
[infinite β]
(f : α → β) :
For s : multiset α, we can lift the existential statement that ∃ x, x ∈ s to a trunc α.
Equations
- trunc_of_multiset_exists_mem s = quotient.rec_on_subsingleton s (λ (l : list α) (h : ∃ (x : α), x ∈ ⟦l⟧), trunc_of_multiset_exists_mem._match_1 l h l h)
- trunc_of_multiset_exists_mem._match_1 l h (a :: _x) _x_1 = trunc.mk a
- trunc_of_multiset_exists_mem._match_1 l h list.nil _x = false.elim _
A fintype with positive cardinality constructively contains an element.
Equations
- trunc_of_card_pos h = let _inst : nonempty α := _ in trunc_of_nonempty_fintype α
def
trunc_sigma_of_exists
{α : Type u_1}
[fintype α]
{P : α → Prop}
[decidable_pred P] :
(∃ (a : α), P a) → trunc (Σ' (a : α), P a)
By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a
to trunc (Σ' a, P a), containing data.
Equations
- trunc_sigma_of_exists h = trunc_of_nonempty_fintype (Σ' (a : α), P a)