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

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

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

Equations

• s.toFinset = Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) Finset.univ

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

@[simp]

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

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.

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

• s.decidableMemOfFintype a = decidable_of_iff (a ∈ s.toFinset) ⋯

@[simp]

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

@[simp]

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

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.

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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.

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.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] : s.toFinset = ∅ ↔ s = ∅

@[simp]

theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] : s.toFinset = Finset.univ ↔ s = univ

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

theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] : s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

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

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

@[simp]

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

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

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

@[simp]

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

Fintype (s : Finset α)

instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) : Fintype { x : α // x ∈ s }

Equations

• s.fintypeCoeSort = { elems := s.attach, complete := ⋯ }

@[simp]

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

theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} : ↑(Finset.image f Finset.univ) = Set.range f

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

Equations

• List.Subtype.fintype l = Fintype.ofList l.attach ⋯

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

Equations

• Multiset.Subtype.fintype s = Fintype.ofMultiset s.attach ⋯

instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) : Fintype { x : α // x ∈ s }

Equations

• Finset.Subtype.fintype s = { elems := s.attach, complete := ⋯ }

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

Equations

• FinsetCoe.fintype s = Finset.Subtype.fintype s

theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} : s.attach = univ

instance Prop.fintype : Fintype Prop

Equations

• «Prop».fintype = { elems := { val := {True, False}, nodup := «Prop».fintype._proof_2 }, complete := «Prop».fintype._proof_3 }

@[simp]

theorem Fintype.univ_Prop : Finset.univ = {True, False}

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

Equations

• Subtype.fintype p = Fintype.subtype (Finset.filter p Finset.univ) ⋯

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

• setFintype s = Subtype.fintype fun (x : α) => x ∈ s

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

• Fintype.finsetEquivSet = { toFun := Finset.toSet, invFun := fun (s : Set α) => s.toFinset, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] : ⇑finsetEquivSet = Finset.toSet

@[simp]

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

@[simp]

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

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

• Fintype.finsetOrderIsoSet = { toEquiv := Fintype.finsetEquivSet, map_rel_iff' := ⋯ }

@[simp]

theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] : finsetOrderIsoSet.toEquiv = finsetEquivSet

@[simp]

theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] : ⇑finsetOrderIsoSet = Finset.toSet

@[simp]

theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] : ⇑finsetOrderIsoSet.symm = ⇑finsetEquivSet.symm

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

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

• finsetStx = Lean.ParserDescr.node `finsetStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "finset% ") (Lean.ParserDescr.cat `term 0))

def precheckFinsetStx : Lean.Elab.Term.Quotation.Precheck

quot_precheck for the finset% syntax.

Equations

• One or more equations did not get rendered due to their size.