Subsets of finite types #

In a Fintype, all Sets are automatically Finsets, and there are only finitely many of them.

Main results #

Set.toFinset: convert a subset of a finite type to a Finset
Finset.fintypeCoeSort: ((s : Finset α) : Type*) is a finite type
Fintype.finsetEquivSet: Finset α and Set α are equivalent if α is a Fintype

source

def Set.toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :

Finset α

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

Equations

Instances For

source

theorem Set.toFinset_congr {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (h : s = t) :

s.toFinset = t.toFinset

source

@[simp]

theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype ↑s] {a : α} :

a ∈ s.toFinset ↔ a ∈ s

source

theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

p.toFinset = s

Many Fintype instances for sets are defined using an extensionally equal Finset. Rewriting s.toFinset with Set.toFinset_ofFinset replaces the term with such a Finset.

source

def Set.decidableMemOfFintype {α : Type u_1} [DecidableEq α] (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

Instances For

source

@[simp]

theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :

↑s.toFinset = s

source

@[simp]

theorem Set.toFinset_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :

s.toFinset.Nonempty ↔ s.Nonempty

source

theorem Set.Aesop.toFinset_nonempty_of_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :

s.Nonempty → s.toFinset.Nonempty

Alias of the reverse direction of Set.toFinset_nonempty.

source

@[simp]

theorem Set.toFinset_inj {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s.toFinset = t.toFinset ↔ s = t

source

theorem Set.toFinset_subset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s.toFinset ⊆ t.toFinset ↔ s ⊆ t

source

theorem Set.toFinset_subset_toFinset_of_subset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s ⊆ t → s.toFinset ⊆ t.toFinset

Alias of the reverse direction of Set.toFinset_subset_toFinset.

source

@[simp]

theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :

s.toFinset ⊂ t ↔ s ⊂ ↑t

source

@[simp]

theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :

s ⊆ t.toFinset ↔ ↑s ⊆ t

source

@[simp]

theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :

s ⊂ t.toFinset ↔ ↑s ⊂ t

source

theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s.toFinset ⊂ t.toFinset ↔ s ⊂ t

source

@[simp]

theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :

s.toFinset ⊆ t ↔ s ⊆ ↑t

source

theorem Set.toFinset_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s ⊆ t → s.toFinset ⊆ t.toFinset

Alias of the reverse direction of Set.toFinset_subset_toFinset.

source

theorem Set.toFinset_strict_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

s ⊂ t → s.toFinset ⊂ t.toFinset

Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

source

@[simp]

theorem Set.disjoint_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :

Disjoint s.toFinset t.toFinset ↔ Disjoint s t

source

@[simp]

theorem Set.toFinset_nontrivial {α : Type u_1} {s : Set α} [Fintype ↑s] :

s.toFinset.Nontrivial ↔ s.Nontrivial

source

@[simp]

theorem Set.toFinset_inter {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∩ t)] :

(s ∩ t).toFinset = s.toFinset ∩ t.toFinset

source

@[simp]

theorem Set.toFinset_union {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∪ t)] :

(s ∪ t).toFinset = s.toFinset ∪ t.toFinset

source

@[simp]

theorem Set.toFinset_diff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s \ t)] :

(s \ t).toFinset = s.toFinset \ t.toFinset

source

@[simp]

theorem Set.toFinset_symmDiff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(symmDiff s t)] :

(symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset

source

@[simp]

theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype ↑s] [Fintype α] [Fintype ↑sᶜ] :

sᶜ.toFinset = s.toFinsetᶜ

source

@[simp]

theorem Set.toFinset_empty {α : Type u_1} [Fintype ↑∅] :

∅.toFinset = ∅

source

@[simp]

theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype ↑univ] :

univ.toFinset = Finset.univ

source

@[simp]

theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] :

s.toFinset = ∅ ↔ s = ∅

source

@[simp]

theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] :

s.toFinset = Finset.univ ↔ s = univ

source

@[simp]

theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype ↑{x : α | p x}] :

{x : α | p x}.toFinset = Finset.filter p Finset.univ

source

theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] :

s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

source

@[simp]

theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set α) [Fintype ↑s] [Fintype ↑(f '' s)] :

(f '' s).toFinset = Finset.image f s.toFinset

source

@[simp]

theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : β → α) [Fintype ↑(range f)] :

(range f).toFinset = Finset.image f Finset.univ

source

@[simp]

theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype ↑{a}] :

{a}.toFinset = {a}

source

@[simp]

theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype ↑s] :

(insert a s).toFinset = insert a s.toFinset

source

theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ s] :

{x : α | x ∈ s} = s.toFinset

source

@[simp]

theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype ↑↑s] :

(↑s).toFinset = s

`Fintype (s : Finset α)` #

source

instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) :

Fintype { x : α // x ∈ s }

Equations

source

@[simp]

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

univ = s.attach

source

theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} :

↑(Finset.image f Finset.univ) = Set.range f

source

instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :

Fintype { x : α // x ∈ l }

Equations

source

instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) :

Fintype { x : α // x ∈ s }

Equations

source

instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :

Fintype { x : α // x ∈ s }

Equations

source

instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :

Fintype ↑↑s

Equations

source

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

s.attach = univ

source

instance Prop.fintype :

Fintype Prop

Equations

source

@[simp]

theorem Fintype.univ_Prop :

Finset.univ = {True , False }

source

instance Subtype.fintype {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype α] :

Fintype { x : α // p x }

Equations

source

def setFintype {α : Type u_1} [Fintype α] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :

Fintype ↑s

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

Equations

Instances For

source

noncomputable def Fintype.finsetEquivSet {α : Type u_1} [Fintype α] :

Finset α ≃ Set α

Given Fintype α, finsetEquivSet is the equiv between Finset α and Set α. (All sets on a finite type are finite.)

Equations

Instances For

source

@[simp]

theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] :

⇑finsetEquivSet = Finset.toSet

source

@[simp]

theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :

finsetEquivSet s = ↑s

source

@[simp]

theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] :

finsetEquivSet.symm s = s.toFinset

source

noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] :

Finset α ≃o Set α

Given a fintype α, finsetOrderIsoSet is the order isomorphism between Finset α and Set α (all sets on a finite type are finite).

Equations

Instances For

source

@[simp]

theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] :

finsetOrderIsoSet.toEquiv = finsetEquivSet

source

@[simp]

theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] :

⇑finsetOrderIsoSet = Finset.toSet

source

@[simp]

theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] :

⇑finsetOrderIsoSet.symm = ⇑finsetEquivSet.symm

source

theorem mem_image_univ_iff_mem_range {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq β] {f : α → β} {b : β} :

b ∈ Finset.image f Finset.univ ↔ b ∈ Set.range f

source

def finsetStx :

Lean.ParserDescr

finset% t elaborates t as a Finset. If t is a Set, then inserts Set.toFinset. Does not make use of the expected type; useful for big operators over finsets.

#check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool

Equations

Instances For

source

def precheckFinsetStx :

Lean.Elab.Term.Quotation.Precheck

quot_precheck for the finset% syntax.

Equations

Instances For

Documentation

Mathlib.Data.Fintype.Sets

Subsets of finite types #

Main results #

`Fintype (s : Finset α)` #

Subsets of finite types #

Main results #

Fintype (s : Finset α) #

`Fintype (s : Finset α)` #