data.fintype.basic - mathlib docs

@[class]

structure fintype (α : Type u_4) :

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 of this typeclass

Instances of other typeclasses for fintype

source

def finset.univ {α : Type u_1} [fintype α] :

finset α

univ is the universal finite set of type finset α implied from the assumption fintype α.

Equations

finset.univ = fintype.elems α

source

@[simp]

theorem finset.mem_univ {α : Type u_1} [fintype α] (x : α) :

x ∈ finset.univ

source

@[simp]

theorem finset.mem_univ_val {α : Type u_1} [fintype α] (x : α) :

x ∈ finset.univ.val

source

theorem finset.eq_univ_iff_forall {α : Type u_1} [fintype α] {s : finset α} :

s = finset.univ ↔ ∀ (x : α), x ∈ s

source

theorem finset.eq_univ_of_forall {α : Type u_1} [fintype α] {s : finset α} :

(∀ (x : α), x ∈ s) → s = finset.univ

source

@[simp, norm_cast]

theorem finset.coe_univ {α : Type u_1} [fintype α] :

↑finset.univ = set.univ

source

@[simp, norm_cast]

theorem finset.coe_eq_univ {α : Type u_1} [fintype α] {s : finset α} :

↑s = set.univ ↔ s = finset.univ

source

theorem finset.nonempty.eq_univ {α : Type u_1} [fintype α] {s : finset α} [subsingleton α] :

s.nonempty → s = finset.univ

source

theorem finset.univ_nonempty_iff {α : Type u_1} [fintype α] :

finset.univ.nonempty ↔ nonempty α

source

theorem finset.univ_nonempty {α : Type u_1} [fintype α] [nonempty α] :

finset.univ.nonempty

source

theorem finset.univ_eq_empty_iff {α : Type u_1} [fintype α] :

finset.univ = ∅ ↔ is_empty α

source

@[simp]

theorem finset.univ_eq_empty {α : Type u_1} [fintype α] [is_empty α] :

finset.univ = ∅

source

@[simp]

theorem finset.univ_unique {α : Type u_1} [fintype α] [unique α] :

finset.univ = {inhabited.default}

source

@[simp]

theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :

s ⊆ finset.univ

source

@[protected, instance]

def finset.bounded_order {α : Type u_1} [fintype α] :

bounded_order (finset α)

Equations

finset.bounded_order = {top := finset.univ _inst_1, le_top := _, bot := order_bot.bot finset.order_bot, bot_le := _}

source

@[simp]

theorem finset.top_eq_univ {α : Type u_1} [fintype α] :

⊤ = finset.univ

source

theorem finset.ssubset_univ_iff {α : Type u_1} [fintype α] {s : finset α} :

s ⊂ finset.univ ↔ s ≠ finset.univ

source

theorem finset.codisjoint_left {α : Type u_1} [fintype α] {s t : finset α} :

codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

source

theorem finset.codisjoint_right {α : Type u_1} [fintype α] {s t : finset α} :

codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s

source

@[protected, instance]

def finset.boolean_algebra {α : Type u_1} [fintype α] [decidable_eq α] :

boolean_algebra (finset α)

Equations

finset.boolean_algebra = generalized_boolean_algebra.to_boolean_algebra

source

theorem finset.sdiff_eq_inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :

s \ t = s ∩ tᶜ

source

theorem finset.compl_eq_univ_sdiff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

sᶜ = finset.univ \ s

source

@[simp]

theorem finset.mem_compl {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :

a ∈ sᶜ ↔ a ∉ s

source

theorem finset.not_mem_compl {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :

a ∉ sᶜ ↔ a ∈ s

source

@[simp, norm_cast]

theorem finset.coe_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

↑sᶜ = (↑s)ᶜ

source

@[simp]

theorem finset.compl_empty {α : Type u_1} [fintype α] [decidable_eq α] :

∅ᶜ = finset.univ

source

@[simp]

theorem finset.compl_univ {α : Type u_1} [fintype α] [decidable_eq α] :

finset.univ ᶜ = ∅

source

@[simp]

theorem finset.compl_eq_empty_iff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

sᶜ = ∅ ↔ s = finset.univ

source

@[simp]

theorem finset.compl_eq_univ_iff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

sᶜ = finset.univ ↔ s = ∅

source

@[simp]

theorem finset.union_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

s ∪ sᶜ = finset.univ

source

@[simp]

theorem finset.inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

s ∩ sᶜ = ∅

source

@[simp]

theorem finset.compl_union {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :

(s ∪ t)ᶜ = sᶜ ∩ tᶜ

source

@[simp]

theorem finset.compl_inter {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :

(s ∩ t)ᶜ = sᶜ ∪ tᶜ

source

@[simp]

theorem finset.compl_erase {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :

(s.erase a)ᶜ = has_insert.insert a sᶜ

source

@[simp]

theorem finset.compl_insert {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :

(has_insert.insert a s)ᶜ = sᶜ.erase a

source

@[simp]

theorem finset.insert_compl_self {α : Type u_1} [fintype α] [decidable_eq α] (x : α) :

has_insert.insert x {x}ᶜ = finset.univ

source

@[simp]

theorem finset.compl_filter {α : Type u_1} [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p] [Π (x : α), decidable (¬p x)] :

(finset.filter p finset.univ)ᶜ = finset.filter (λ (x : α), ¬p x) finset.univ

source

theorem finset.compl_ne_univ_iff_nonempty {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

sᶜ ≠ finset.univ ↔ s.nonempty

source

theorem finset.compl_singleton {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :

{a}ᶜ = finset.univ.erase a

source

theorem finset.insert_inj_on' {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

set.inj_on (λ (a : α), has_insert.insert a s) ↑sᶜ

source

theorem finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq α] [fintype β] {f : β → α} (hf : function.surjective f) :

finset.image f finset.univ = finset.univ

source

theorem finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : β ↪ α} (hf : function.surjective ⇑f) :

finset.map f finset.univ = finset.univ

source

@[simp]

theorem finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : β ≃ α) :

finset.map f.to_embedding finset.univ = finset.univ

source

@[simp]

theorem finset.univ_inter {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

finset.univ ∩ s = s

source

@[simp]

theorem finset.inter_univ {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :

s ∩ finset.univ = s

source

@[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

source

theorem finset.piecewise_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) [Π (i : α), decidable (i ∈ s)] [Π (i : α), decidable (i ∈ sᶜ)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :

sᶜ.piecewise f g = s.piecewise g f

source

@[simp]

theorem finset.piecewise_erase_univ {α : Type u_1} [fintype α] {δ : α → Sort u_2} [decidable_eq α] (a : α) (f g : Π (a : α), δ a) :

(finset.univ.erase a).piecewise f g = function.update f a (g a)

source

theorem finset.univ_map_equiv_to_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (e : α ≃ β) :

finset.map e.to_embedding finset.univ = finset.univ

source

@[simp]

theorem finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), ∃ (x : α), f x = y)] [decidable_eq β] :

finset.filter (λ (y : β), ∃ (x : α), f x = y) finset.univ = finset.image f finset.univ

source

theorem finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), y ∈ set.range f)] [decidable_eq β] :

finset.filter (λ (y : β), y ∈ set.range f) finset.univ = finset.image f finset.univ

Note this is a special case of (finset.image_preimage f univ _).symm.

source

theorem finset.coe_filter_univ {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :

↑(finset.filter p finset.univ) = {x : α | p x}

source

@[protected, 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) _

source

@[protected, 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

source

@[protected, 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

source

@[protected, instance]

def fintype.decidable_mem_range_fintype {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α → β) :

decidable_pred (λ (_x : β), _x ∈ set.range f)

Equations

fintype.decidable_mem_range_fintype f = λ (x : β), fintype.decidable_exists_fintype

source

@[protected, 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) _

source

@[protected, instance]

def fintype.decidable_eq_embedding_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :

decidable_eq (α ↪ β)

Equations

fintype.decidable_eq_embedding_fintype = λ (a b : α ↪ β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_one_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_one α] [has_one β] :

decidable_eq (one_hom α β)

Equations

fintype.decidable_eq_one_hom_fintype = λ (a b : one_hom α β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_zero α] [has_zero β] :

decidable_eq (zero_hom α β)

Equations

fintype.decidable_eq_zero_hom_fintype = λ (a b : zero_hom α β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_mul_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_mul α] [has_mul β] :

decidable_eq (α →ₙ* β)

Equations

fintype.decidable_eq_mul_hom_fintype = λ (a b : α →ₙ* β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_add_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_add α] [has_add β] :

decidable_eq (add_hom α β)

Equations

fintype.decidable_eq_add_hom_fintype = λ (a b : add_hom α β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_add_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [add_zero_class α] [add_zero_class β] :

decidable_eq (α →+ β)

Equations

fintype.decidable_eq_add_monoid_hom_fintype = λ (a b : α →+ β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [mul_one_class α] [mul_one_class β] :

decidable_eq (α →* β)

Equations

fintype.decidable_eq_monoid_hom_fintype = λ (a b : α →* β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_monoid_with_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [mul_zero_one_class α] [mul_zero_one_class β] :

decidable_eq (α →*₀ β)

Equations

fintype.decidable_eq_monoid_with_zero_hom_fintype = λ (a b : α →*₀ β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_eq_ring_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [semiring α] [semiring β] :

decidable_eq (α →+* β)

Equations

fintype.decidable_eq_ring_hom_fintype = λ (a b : α →+* β), decidable_of_iff (⇑a = ⇑b) _

source

@[protected, instance]

def fintype.decidable_injective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] :

decidable_pred function.injective

Equations

fintype.decidable_injective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype

source

@[protected, instance]

def fintype.decidable_surjective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [fintype β] :

decidable_pred function.surjective

Equations

fintype.decidable_surjective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype

source

@[protected, instance]

def fintype.decidable_bijective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :

decidable_pred function.bijective

Equations

fintype.decidable_bijective_fintype = λ (x : α → β), _.mpr and.decidable

source

@[protected, instance]

def fintype.decidable_right_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :

decidable (function.right_inverse f g)

Equations

fintype.decidable_right_inverse_fintype f g = show decidable (∀ (x : α), g (f x) = x), from fintype.decidable_forall_fintype

source

@[protected, instance]

def fintype.decidable_left_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :

decidable (function.left_inverse f g)

Equations

fintype.decidable_left_inverse_fintype f g = show decidable (∀ (x : β), f (g x) = x), from fintype.decidable_forall_fintype

source

def fintype.of_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) (H : ∀ (x : α), x ∈ s) :

fintype α

Construct a proof of fintype α from a universal multiset

Equations

fintype.of_multiset s H = {elems := s.to_finset, complete := _}

source

def fintype.of_list {α : Type u_1} [decidable_eq α] (l : list α) (H : ∀ (x : α), x ∈ l) :

fintype α

Construct a proof of fintype α from a universal list

Equations

fintype.of_list l H = {elems := l.to_finset, complete := _}

source

@[protected, instance]

def fintype.subsingleton (α : Type u_1) :

subsingleton (fintype α)

source

@[protected]

def fintype.subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ p x) :

fintype {x // p x}

Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.

Equations

fintype.subtype s H = {elems := {val := multiset.pmap subtype.mk s.val _, nodup := _}, complete := _}

source

def fintype.of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

fintype ↥p

Construct a fintype from a finset with the same elements.

Equations

fintype.of_finset s H = fintype.subtype s H

source

def fintype.of_bijective {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) (H : 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 := _}

source

def fintype.of_surjective {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] (f : α → β) (H : 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 := _}

source

@[protected, instance]

def finset.decidable_codisjoint {α : Type u_1} [fintype α] [decidable_eq α] {s t : finset α} :

decidable (codisjoint s t)

Equations

finset.decidable_codisjoint = decidable_of_iff (∀ ⦃a : α⦄, a ∉ s → a ∈ t) finset.decidable_codisjoint._proof_1

source

@[protected, instance]

def finset.decidable_is_compl {α : Type u_1} [fintype α] [decidable_eq α] {s t : finset α} :

decidable (is_compl s t)

Equations

finset.decidable_is_compl = decidable_of_iff' (disjoint s t ∧ codisjoint s t) finset.decidable_is_compl._proof_1

source

def function.injective.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :

↥(set.range f) → α

The inverse of an hf : injective function f : α → β, of the type ↥(set.range f) → α. This is the computable version of function.inv_fun that requires fintype α and decidable_eq β, or the function version of applying (equiv.of_injective f hf).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = fintype.card α.

Equations

hf.inv_of_mem_range = λ (b : ↥(set.range f)), finset.choose (λ (a : α), f a = ↑b) finset.univ _

source

theorem function.injective.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (b : ↥(set.range f)) :

f (hf.inv_of_mem_range b) = ↑b

source

@[simp]

theorem function.injective.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (a : α) :

hf.inv_of_mem_range ⟨f a, _⟩ = a

source

theorem function.injective.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) [nonempty α] :

(set.range f).restrict (function.inv_fun f) = hf.inv_of_mem_range

source

theorem function.injective.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :

function.surjective hf.inv_of_mem_range

source

def function.embedding.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (b : ↥(set.range ⇑f)) :

α

The inverse of an embedding f : α ↪ β, of the type ↥(set.range f) → α. This is the computable version of function.inv_fun that requires fintype α and decidable_eq β, or the function version of applying (equiv.of_injective f f.injective).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = fintype.card α.

Equations

f.inv_of_mem_range b = _.inv_of_mem_range b

source

@[simp]

theorem function.embedding.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (b : ↥(set.range ⇑f)) :

⇑f (f.inv_of_mem_range b) = ↑b

source

@[simp]

theorem function.embedding.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (a : α) :

f.inv_of_mem_range ⟨⇑f a, _⟩ = a

source

theorem function.embedding.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) [nonempty α] :

(set.range ⇑f).restrict (function.inv_fun ⇑f) = f.inv_of_mem_range

source

theorem function.embedding.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) :

function.surjective f.inv_of_mem_range

source

noncomputable def fintype.of_injective {α : Type u_1} {β : Type u_2} [fintype β] (f : α → β) (H : function.injective f) :

fintype α

Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.

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 := _})

source

def fintype.of_equiv {β : Type u_2} (α : Type u_1) [fintype α] (f : α ≃ β) :

fintype β

If f : α ≃ β and α is a fintype, then β is also a fintype.

Equations

fintype.of_equiv α f = fintype.of_bijective ⇑f _

source

def fintype.of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

fintype α

Any subsingleton type with a witness is a fintype (with one term).

Equations

fintype.of_subsingleton a = {elems := {a}, complete := _}

source

@[simp]

theorem fintype.univ_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

finset.univ = {a}

source

@[protected, instance]

def fintype.of_is_empty {α : Type u_1} [is_empty α] :

fintype α

Equations

fintype.of_is_empty = {elems := ∅, complete := _}

source

@[simp, nolint]

theorem fintype.univ_of_is_empty {α : Type u_1} [is_empty α] :

finset.univ = ∅

Note: this lemma is specifically about fintype.of_is_empty. For a statement about arbitrary fintype instances, use finset.univ_eq_empty.

source

def set.to_finset {α : Type u_1} (s : set α) [fintype ↥s] :

finset α

Construct a finset enumerating a set s, given a fintype instance.

Equations

s.to_finset = finset.map (function.embedding.subtype (λ (x : α), x ∈ s)) finset.univ

source

theorem set.to_finset_congr {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] (h : s = t) :

s.to_finset = t.to_finset

source

@[simp]

theorem set.mem_to_finset {α : Type u_1} {s : set α} [fintype ↥s] {a : α} :

a ∈ s.to_finset ↔ a ∈ s

source

theorem set.to_finset_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

p.to_finset = s

Many fintype instances for sets are defined using an extensionally equal finset. Rewriting s.to_finset with set.to_finset_of_finset replaces the term with such a finset.

source

def set.decidable_mem_of_fintype {α : Type u_1} [decidable_eq α] (s : set α) [fintype ↥s] (a : α) :

decidable (a ∈ s)

Membership of a set with a fintype instance is decidable.

Using this as an instance leads to potential loops with subtype.fintype under certain decidability assumptions, so it should only be declared a local instance.

Equations

s.decidable_mem_of_fintype a = decidable_of_iff (a ∈ s.to_finset) set.mem_to_finset

source

@[simp]

theorem set.coe_to_finset {α : Type u_1} (s : set α) [fintype ↥s] :

↑(s.to_finset) = s

source

@[simp]

theorem set.to_finset_nonempty {α : Type u_1} {s : set α} [fintype ↥s] :

s.to_finset.nonempty ↔ s.nonempty

source

@[simp]

theorem set.to_finset_inj {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

s.to_finset = t.to_finset ↔ s = t

source

theorem set.to_finset_subset_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

s.to_finset ⊆ t.to_finset ↔ s ⊆ t

source

@[simp]

theorem set.to_finset_ssubset {α : Type u_1} {s : set α} [fintype ↥s] {t : finset α} :

s.to_finset ⊂ t ↔ s ⊂ ↑t

source

@[simp]

theorem set.subset_to_finset {α : Type u_1} {t : set α} {s : finset α} [fintype ↥t] :

s ⊆ t.to_finset ↔ ↑s ⊆ t

source

@[simp]

theorem set.ssubset_to_finset {α : Type u_1} {t : set α} {s : finset α} [fintype ↥t] :

s ⊂ t.to_finset ↔ ↑s ⊂ t

source

theorem set.to_finset_ssubset_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

s.to_finset ⊂ t.to_finset ↔ s ⊂ t

source

@[simp]

theorem set.to_finset_subset {α : Type u_1} {s : set α} [fintype ↥s] {t : finset α} :

s.to_finset ⊆ t ↔ s ⊆ ↑t

source

theorem set.to_finset_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

s ⊆ t → s.to_finset ⊆ t.to_finset

Alias of the reverse direction of set.to_finset_subset_to_finset.

source

theorem set.to_finset_strict_mono {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

s ⊂ t → s.to_finset ⊂ t.to_finset

Alias of the reverse direction of set.to_finset_ssubset_to_finset.

source

@[simp]

theorem set.disjoint_to_finset {α : Type u_1} {s t : set α} [fintype ↥s] [fintype ↥t] :

disjoint s.to_finset t.to_finset ↔ disjoint s t

source

@[simp]

theorem set.to_finset_inter {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∩ t)] :

(s ∩ t).to_finset = s.to_finset ∩ t.to_finset

source

@[simp]

theorem set.to_finset_union {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∪ t)] :

(s ∪ t).to_finset = s.to_finset ∪ t.to_finset

source

@[simp]

theorem set.to_finset_diff {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s \ t)] :

(s \ t).to_finset = s.to_finset \ t.to_finset

source

@[simp]

theorem set.to_finset_symm_diff {α : Type u_1} (s t : set α) [decidable_eq α] [fintype ↥s] [fintype ↥t] [fintype ↥(s ∆ t)] :

(s ∆ t).to_finset = s.to_finset ∆ t.to_finset

source

@[simp]

theorem set.to_finset_compl {α : Type u_1} (s : set α) [decidable_eq α] [fintype ↥s] [fintype α] [fintype ↥sᶜ] :

sᶜ.to_finset = s.to_finset ᶜ

source

@[simp]

theorem set.to_finset_empty {α : Type u_1} [fintype ↥∅] :

∅.to_finset = ∅

source

@[simp]

theorem set.to_finset_univ {α : Type u_1} [fintype α] [fintype ↥set.univ] :

set.univ.to_finset = finset.univ

source

@[simp]

theorem set.to_finset_eq_empty {α : Type u_1} {s : set α} [fintype ↥s] :

s.to_finset = ∅ ↔ s = ∅

source

@[simp]

theorem set.to_finset_eq_univ {α : Type u_1} {s : set α} [fintype α] [fintype ↥s] :

s.to_finset = finset.univ ↔ s = set.univ

source

@[simp]

theorem set.to_finset_set_of {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] [fintype ↥{x : α | p x}] :

{x : α | p x}.to_finset = finset.filter p finset.univ

source

@[simp]

theorem set.to_finset_ssubset_univ {α : Type u_1} [fintype α] {s : set α} [fintype ↥s] :

s.to_finset ⊂ finset.univ ↔ s ⊂ set.univ

source

@[simp]

theorem set.to_finset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : set α) [fintype ↥s] [fintype ↥(f '' s)] :

(f '' s).to_finset = finset.image f s.to_finset

source

@[simp]

theorem set.to_finset_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype β] (f : β → α) [fintype ↥(set.range f)] :

(set.range f).to_finset = finset.image f finset.univ

source

theorem set.to_finset_singleton {α : Type u_1} (a : α) [fintype ↥{a}] :

{a}.to_finset = {a}

source

@[simp]

theorem set.to_finset_insert {α : Type u_1} [decidable_eq α] {a : α} {s : set α} [fintype ↥(has_insert.insert a s)] [fintype ↥s] :

(has_insert.insert a s).to_finset = has_insert.insert a s.to_finset

source

theorem set.filter_mem_univ_eq_to_finset {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] [decidable_pred (λ (_x : α), _x ∈ s)] :

finset.filter (λ (_x : α), _x ∈ s) finset.univ = s.to_finset

source

@[simp]

theorem finset.to_finset_coe {α : Type u_1} (s : finset α) [fintype ↥↑s] :

↑s.to_finset = s

source

@[protected, instance]

def fin.fintype (n : ℕ) :

fintype (fin n)

Equations

fin.fintype n = {elems := {val := ↑(list.fin_range n), nodup := _}, complete := _}

source

theorem fin.univ_def (n : ℕ) :

finset.univ = {val := ↑(list.fin_range n), nodup := _}

source

@[simp]

theorem fin.image_succ_above_univ {n : ℕ} (i : fin (n + 1)) :

finset.image ⇑(i.succ_above) finset.univ = {i}ᶜ

source

@[simp]

theorem fin.image_succ_univ (n : ℕ) :

finset.image fin.succ finset.univ = {0}ᶜ

source

@[simp]

theorem fin.image_cast_succ (n : ℕ) :

finset.image ⇑fin.cast_succ finset.univ = {fin.last n}ᶜ

source

theorem fin.univ_succ (n : ℕ) :

finset.univ = finset.cons 0 (finset.map {to_fun := fin.succ n, inj' := _} finset.univ) _

Embed fin n into fin (n + 1) by prepending zero to the univ

source

theorem fin.univ_cast_succ (n : ℕ) :

finset.univ = finset.cons (fin.last n) (finset.map fin.cast_succ.to_embedding finset.univ) _

Embed fin n into fin (n + 1) by appending a new fin.last n to the univ

source

theorem fin.univ_succ_above (n : ℕ) (p : fin (n + 1)) :

finset.univ = finset.cons p (finset.map p.succ_above.to_embedding finset.univ) _

Embed fin n into fin (n + 1) by inserting around a specified pivot p : fin (n + 1) into the univ

source

@[instance]

def unique.fintype {α : Type u_1} [unique α] :

fintype α

Equations

unique.fintype = fintype.of_subsingleton inhabited.default

source

@[protected, instance]

def fintype.subtype_eq {α : Type u_1} (y : α) :

fintype {x // x = y}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations

fintype.subtype_eq y = fintype.subtype {y} _

source

@[protected, instance]

def fintype.subtype_eq' {α : Type u_1} (y : α) :

fintype {x // y = x}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations

fintype.subtype_eq' y = fintype.subtype {y} _

source

@[simp]

theorem fintype.univ_empty :

finset.univ = ∅

source

@[simp]

theorem fintype.univ_pempty :

finset.univ = ∅

source

@[protected, instance]

def unit.fintype :

fintype unit

Equations

unit.fintype = fintype.of_subsingleton unit.star()

source

theorem fintype.univ_unit :

finset.univ = {unit.star()}

source

@[protected, instance]

def punit.fintype :

fintype punit

Equations

punit.fintype = fintype.of_subsingleton punit.star

source

@[simp]

theorem fintype.univ_punit :

finset.univ = {punit.star}

source

@[protected, instance]

def bool.fintype :

fintype bool

Equations

bool.fintype = {elems := {val := {bool.tt, bool.ff}, nodup := bool.fintype._proof_1}, complete := bool.fintype._proof_2}

source

@[simp]

theorem fintype.univ_bool :

finset.univ = {bool.tt, bool.ff}

source

@[protected, instance]

def additive.fintype {α : Type u_1} [fintype α] :

fintype (additive α)

Equations

additive.fintype = id

source

@[protected, instance]

def multiplicative.fintype {α : Type u_1} [fintype α] :

fintype (multiplicative α)

Equations

multiplicative.fintype = id

source

def fintype.prod_left {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype (α × β)] [nonempty β] :

fintype α

Given that α × β is a fintype, α is also a fintype.

Equations

fintype.prod_left = {elems := finset.image prod.fst (fintype.elems (α × β)), complete := _}

source

def fintype.prod_right {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype (α × β)] [nonempty α] :

fintype β

Given that α × β is a fintype, β is also a fintype.

Equations

fintype.prod_right = {elems := finset.image prod.snd (fintype.elems (α × β)), complete := _}

source

@[protected, instance]

def ulift.fintype (α : Type u_1) [fintype α] :

fintype (ulift α)

Equations

ulift.fintype α = fintype.of_equiv α equiv.ulift.symm

source

@[protected, instance]

def plift.fintype (α : Type u_1) [fintype α] :

fintype (plift α)

Equations

plift.fintype α = fintype.of_equiv α equiv.plift.symm

source

@[protected, instance]

def order_dual.fintype (α : Type u_1) [fintype α] :

fintype αᵒᵈ

Equations

order_dual.fintype α = _inst_1

source

@[protected, instance]

def order_dual.finite (α : Type u_1) [finite α] :

finite αᵒᵈ

source

@[protected, instance]

def lex.fintype (α : Type u_1) [fintype α] :

fintype (lex α)

Equations

lex.fintype α = _inst_1

source

@[protected, instance]

def finset.fintype_coe_sort {α : Type u} (s : finset α) :

fintype ↥s

Equations

s.fintype_coe_sort = {elems := s.attach, complete := _}

source

@[simp]

theorem finset.univ_eq_attach {α : Type u} (s : finset α) :

finset.univ = s.attach

source

theorem fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :

↑(finset.image f finset.univ) = set.range f

source

@[protected, instance]

def list.subtype.fintype {α : Type u_1} [decidable_eq α] (l : list α) :

fintype {x // x ∈ l}

Equations

list.subtype.fintype l = fintype.of_list l.attach _

source

@[protected, instance]

def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :

fintype {x // x ∈ s}

Equations

multiset.subtype.fintype s = fintype.of_multiset s.attach _

source

@[protected, instance]

def finset.subtype.fintype {α : Type u_1} (s : finset α) :

fintype {x // x ∈ s}

Equations

finset.subtype.fintype s = {elems := s.attach, complete := _}

source

@[protected, instance]

def finset_coe.fintype {α : Type u_1} (s : finset α) :

fintype ↥↑s

Equations

finset_coe.fintype s = finset.subtype.fintype s

source

theorem finset.attach_eq_univ {α : Type u_1} {s : finset α} :

s.attach = finset.univ

source

@[protected, instance]

def plift.fintype_Prop (p : Prop) [decidable p] :

fintype (plift p)

Equations

plift.fintype_Prop p = {elems := dite p (λ (h : p), {{down := h}}) (λ (h : ¬p), ∅), complete := _}

source

@[protected, instance]

def Prop.fintype :

fintype Prop

Equations

Prop.fintype = {elems := {val := {true, false}, nodup := Prop.fintype._proof_1}, complete := Prop.fintype._proof_2}

source

@[simp]

theorem fintype.univ_Prop :

finset.univ = {true, false}

source

@[protected, instance]

def subtype.fintype {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype α] :

fintype {x // p x}

Equations

subtype.fintype p = fintype.subtype (finset.filter p finset.univ) _

source

def set_fintype {α : Type u_1} [fintype α] (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :

fintype ↥s

A set on a fintype, when coerced to a type, is a fintype.

Equations

set_fintype s = subtype.fintype (λ (x : α), x ∈ s)

source

@[simp]

theorem coe_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1}) :

↑(⇑((units_equiv_prod_subtype α).symm) p) = ↑p.fst

source

@[simp]

theorem units_equiv_prod_subtype_apply_coe (α : Type u_1) [monoid α] (u : αˣ) :

↑(⇑(units_equiv_prod_subtype α) u) = (↑u, ↑u⁻¹)

source

@[simp]

theorem coe_inv_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1}) :

↑(⇑((units_equiv_prod_subtype α).symm) p)⁻¹ = ↑p.snd

source

def units_equiv_prod_subtype (α : Type u_1) [monoid α] :

αˣ ≃ {p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1}

The αˣ type is equivalent to a subtype of α × α.

Equations

units_equiv_prod_subtype α = {to_fun := λ (u : αˣ), ⟨(↑u, ↑u⁻¹), _⟩, inv_fun := λ (p : {p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1}), {val := ↑p.fst, inv := ↑p.snd, val_inv := _, inv_val := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem units_equiv_ne_zero_apply_coe (α : Type u_1) [group_with_zero α] (a : αˣ) :

↑(⇑(units_equiv_ne_zero α) a) = ↑a

source

def units_equiv_ne_zero (α : Type u_1) [group_with_zero α] :

αˣ ≃ {a // a ≠ 0}

In a group_with_zero α, the unit group αˣ is equivalent to the subtype of nonzero elements.

Equations

units_equiv_ne_zero α = {to_fun := λ (a : αˣ), ⟨↑a, _⟩, inv_fun := λ (a : {a // a ≠ 0}), units.mk0 ↑a _, left_inv := _, right_inv := _}

source

@[simp]

theorem units_equiv_ne_zero_symm_apply (α : Type u_1) [group_with_zero α] (a : {a // a ≠ 0}) :

⇑((units_equiv_ne_zero α).symm) a = units.mk0 ↑a _

source

noncomputable def fintype.finset_equiv_set {α : Type u_1} [fintype α] :

finset α ≃ set α

Given fintype α, finset_equiv_set is the equiv between finset α and set α. (All sets on a finite type are finite.)

Equations

fintype.finset_equiv_set = {to_fun := coe coe_to_lift, inv_fun := λ (s : set α), s.to_finset, left_inv := _, right_inv := _}

source

@[simp]

theorem fintype.finset_equiv_set_apply {α : Type u_1} [fintype α] (s : finset α) :

⇑fintype.finset_equiv_set s = ↑s

source

@[simp]

theorem fintype.finset_equiv_set_symm_apply {α : Type u_1} [fintype α] (s : set α) [fintype ↥s] :

⇑(fintype.finset_equiv_set.symm) s = s.to_finset

source

@[protected, instance]

def quotient.fintype {α : Type u_1} [fintype α] (s : setoid α) [decidable_rel has_equiv.equiv] :

fintype (quotient s)

Equations

quotient.fintype s = fintype.of_surjective quotient.mk _

source

@[protected, instance]

def psigma.fintype_prop_left {α : Prop} {β : α → Type u_1} [decidable α] [Π (a : α), fintype (β a)] :

fintype (Σ' (a : α), β a)

Equations

psigma.fintype_prop_left = dite α (λ (h : α), fintype.of_equiv (β h) {to_fun := λ (x : β h), ⟨h, x⟩, inv_fun := psigma.snd (λ (a : α), β a), left_inv := _, right_inv := _}) (λ (h : ¬α), {elems := ∅, complete := _})

source

@[protected, 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⟩

source

@[protected, instance]

def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :

fintype (Σ' (a : α), β a)

Equations

psigma.fintype_prop_prop = dite (∃ (a : α), β a) (λ (h : ∃ (a : α), β a), {elems := {⟨_, _⟩}, complete := _}) (λ (h : ¬∃ (a : α), β a), {elems := ∅, complete := _})

source

@[protected, instance]

def pfun_fintype (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), fintype (α hp)] :

fintype (Π (hp : p), α hp)

Equations

pfun_fintype p α = dite p (λ (hp : p), fintype.of_equiv (α hp) {to_fun := λ (a : α hp) (_x : p), a, inv_fun := λ (f : Π (hp : p), α hp), f hp, left_inv := _, right_inv := _}) (λ (hp : ¬p), {elems := {λ (h : p), _.elim}, complete := _})

source

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

source

def fintype.choose_x {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :

{a // p a}

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of the corresponding subtype.

Equations

fintype.choose_x p hp = ⟨finset.choose p finset.univ _, _⟩

source

def fintype.choose {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :

α

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of α.

Equations

fintype.choose p hp = ↑(fintype.choose_x p hp)

source

theorem fintype.choose_spec {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :

p (fintype.choose p hp)

source

@[simp]

theorem fintype.choose_subtype_eq {α : Type u_1} (p : α → Prop) [fintype {a // p a}] [decidable_eq α] (x : {a // p a}) (h : (∃! (a : {a // p a}), ↑a = ↑x) := _) :

fintype.choose (λ (y : {a // p a}), ↑y = ↑x) h = x

source

def fintype.bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) (b : β) :

α

bij_inv f is the unique inverse to a bijection f. This acts as a computable alternative to function.inv_fun.

Equations

fintype.bij_inv f_bij b = fintype.choose (λ (a : α), f a = b) _

source

theorem fintype.left_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

function.left_inverse (fintype.bij_inv f_bij) f

source

theorem fintype.right_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

function.right_inverse (fintype.bij_inv f_bij) f

source

theorem fintype.bijective_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :

function.bijective (fintype.bij_inv f_bij)

source

def trunc_of_multiset_exists_mem {α : Type u_1} (s : multiset α) :

(∃ (x : α), x ∈ s) → trunc α

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 _

source

def trunc_of_nonempty_fintype (α : Type u_1) [nonempty α] [fintype α] :

trunc α

A nonempty fintype constructively contains an element.

Equations

trunc_of_nonempty_fintype α = trunc_of_multiset_exists_mem finset.univ.val _

source

def trunc_sigma_of_exists {α : Type u_1} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ (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)

source

@[simp]

theorem multiset.count_univ {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :

multiset.count a finset.univ.val = 1

source

noncomputable def seq_of_forall_finset_exists_aux {α : Type u_1} [decidable_eq α] (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), ∃ (y : α), (∀ (x : α), x ∈ s → P x) → (P y ∧ ∀ (x : α), x ∈ s → r x y)) :

ℕ → α

Auxiliary definition to show exists_seq_of_forall_finset_exists.

Equations

seq_of_forall_finset_exists_aux P r h n = classical.some _

source

theorem exists_seq_of_forall_finset_exists {α : Type u_1} (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), (∀ (x : α), x ∈ s → P x) → (∃ (y : α), P y ∧ ∀ (x : α), x ∈ s → r x y)) :

∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Induction principle to build a sequence, by adding one point at a time satisfying a given relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m < n. We also ensure that all constructed points satisfy a given predicate P.

source

theorem exists_seq_of_forall_finset_exists' {α : Type u_1} (P : α → Prop) (r : α → α → Prop) [is_symm α r] (h : ∀ (s : finset α), (∀ (x : α), x ∈ s → P x) → (∃ (y : α), P y ∧ ∀ (x : α), x ∈ s → r x y)) :

∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)

Induction principle to build a sequence, by adding one point at a time satisfying a given symmetric relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m ≠ n. We also ensure that all constructed points satisfy a given predicate P.

mathlib documentation

Finite types #

Main declarations #

Instances #

`fintype (s : finset α)` #

Finite types #

Main declarations #

Instances #

fintype (s : finset α) #

`fintype (s : finset α)` #