Documentation

Mathlib.Data.Fintype.Sets

Subsets of finite types #

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

Main results #

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

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

Equations
theorem Set.toFinset_congr {α : Type u_1} {s t : Set α} [Fintype s] [Fintype t] (h : s = t) :
@[simp]
theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype s] {a : α} :
theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x s x p) :

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 : α) :

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

Alias of the reverse direction of Set.toFinset_nonempty.

@[simp]
theorem Set.toFinset_inj {α : Type u_1} {s t : Set α} [Fintype s] [Fintype t] :
theorem Set.toFinset_subset_toFinset {α : Type u_1} {s t : Set α} [Fintype s] [Fintype 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] :
@[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 ts.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 ts.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] :
@[simp]
theorem Set.toFinset_nontrivial {α : Type u_1} {s : Set α} [Fintype s] :
@[simp]
theorem Set.toFinset_inter {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s t)] :
@[simp]
theorem Set.toFinset_union {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s t)] :
@[simp]
theorem Set.toFinset_diff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype ↑(s \ t)] :
@[simp]
theorem Set.toFinset_symmDiff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] [Fintype (symmDiff s t)] :
@[simp]
theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype s] [Fintype α] [Fintype s] :
@[simp]
theorem Set.toFinset_empty {α : Type u_1} [Fintype ] :
@[simp]
@[simp]
theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype s] :
@[simp]
theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype s] :
@[simp]
theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : αProp) [DecidablePred p] [Fintype {x : α | p x}] :
@[simp]
theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αβ) (s : Set α) [Fintype s] [Fintype ↑(f '' s)] :
@[simp]
theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : βα) [Fintype (range f)] :
@[simp]
theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype {a}] :
@[simp]
theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype (insert a s)] [Fintype s] :
theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype s] [DecidablePred fun (x : α) => x s] :
Finset.filter (fun (x : α) => x s) Finset.univ = 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
@[simp]
theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) :
theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : αβ} :
instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :
Fintype { x : α // x l }
Equations
instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :
Fintype { x : α // x s }
Equations
instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :
Fintype s
Equations
theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} :
Equations
instance Subtype.fintype {α : Type u_1} (p : αProp) [DecidablePred p] [Fintype α] :
Fintype { x : α // p x }
Equations
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
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
@[simp]
theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :
@[simp]
noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] :

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

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

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

quot_precheck for the finset% syntax.

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