mathlib3 documentation

logic.equiv.fintype

Equivalence between fintypes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains some basic results on equivalences where one or both sides of the equivalence are fintypes.

Main definitions #

Implementation details #

def function.embedding.to_equiv_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) :

Computably turn an embedding f : α ↪ β into an equiv α ≃ set.range f, if α is a fintype. Has poor computational performance, due to exhaustive searching in constructed inverse. When a better inverse is known, use equiv.of_left_inverse' or equiv.of_left_inverse instead. This is the computable version of equiv.of_injective.

Equations
@[simp]
theorem function.embedding.to_equiv_range_apply {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (a : α) :
(f.to_equiv_range) a = f a, _⟩
@[simp]
theorem function.embedding.to_equiv_range_symm_apply_self {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (a : α) :
def equiv.perm.via_fintype_embedding {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) :

Extend the domain of e : equiv.perm α, mapping it through f : α ↪ β. Everything outside of set.range f is kept fixed. Has poor computational performance, due to exhaustive searching in constructed inverse due to using function.embedding.to_equiv_range. When a better α ≃ set.range f is known, use equiv.perm.via_set_range. When [fintype α] is not available, a noncomputable version is available as equiv.perm.via_embedding.

Equations
@[simp]
theorem equiv.perm.via_fintype_embedding_apply_image {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) (a : α) :
theorem equiv.perm.via_fintype_embedding_apply_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) {b : β} (h : b set.range f) :
theorem equiv.perm.via_fintype_embedding_apply_not_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) {b : β} (h : b set.range f) :
noncomputable def equiv.to_compl {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) :
{x // ¬p x} {x // ¬q x}

If e is an equivalence between two subtypes of a fintype α, e.to_compl is an equivalence between the complement of those subtypes.

See also equiv.compl, for a computable version when a term of type {e' : α ≃ α // ∀ x : {x // p x}, e' x = e x} is known.

Equations
@[reducible]
noncomputable def equiv.extend_subtype {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) :

If e is an equivalence between two subtypes of a fintype α, e.extend_subtype is a permutation of α acting like e on the subtypes and doing something arbitrary outside.

Note that when p = q, equiv.perm.subtype_congr e (equiv.refl _) can be used instead.

theorem equiv.extend_subtype_apply_of_mem {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) (x : α) (hx : p x) :
(e.extend_subtype) x = (e x, hx⟩)
theorem equiv.extend_subtype_mem {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) (x : α) (hx : p x) :
theorem equiv.extend_subtype_apply_of_not_mem {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) (x : α) (hx : ¬p x) :
theorem equiv.extend_subtype_not_mem {α : Type u_1} [fintype α] {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) (x : α) (hx : ¬p x) :