`Finset`: 有限集合¶

Finset α は，型 α の元からなる有限集合です．リストとは違い，重複を持たない集合として扱います．一方で，有限集合なので card，有限和 ∑，有限積 ∏ などを使えます． Finset α は Set α に有限性を付けたものというより，有限個の要素をデータとして持つ型です．そのため，計算や有限和・有限積との相性がよい一方，一般の集合論的な部分集合は Set α で表します．

Mathlib では，有限な対象や集合的な対象を表す方法がいくつかあります．

List α: 順序と重複を持つ有限列です．計算や再帰に向いています．
Multiset α: 順序を無視し，重複は残す有限多重集合です．
Set α: α → Prop として実装される，型 α の部分集合です．有限とは限りません．
Finset α: 順序も重複も無視する有限集合です．有限和や有限積の添字に向いています．
Fintype α: 型 α のすべての元が有限個である，という型クラスです．
Subtype: 条件を満たす元を新しい型として扱う方法です．

したがって，順序つきのデータとして扱いたいなら List，重複個数を気にするなら Multiset，有限集合として和や濃度を扱いたいなら Finset，型 α の一般の部分集合なら Set α を使います．

多くの操作では，元の等号を判定できること，つまり [DecidableEq α] が必要になります．自然数 Nat にはそのインスタンスがあるため，次の例はそのまま動きます．たとえば，要素を挿入したときに既に含まれているかどうかを判定するには，要素同士の等号を決定できる必要があります．

#check List
#check Multiset
#check Finset
#check Fintype

def finsetSectionList : List Nat :=
  [1, 2, 1]

#eval finsetSectionList

def finsetSectionMultiset : Multiset Nat :=
  finsetSectionList

#eval finsetSectionMultiset

def finsetSectionFinset : Finset Nat :=
  {1, 1, 2}

#eval finsetSectionFinset
#eval finsetSectionFinset.card

List は順序と重複をそのまま持つため [1, 2, 1] と表示されます． Multiset は順序を無視しますが，重複は残します． Finset は重複を消すので，{1, 1, 2} から作っても中身は {1, 2} になります．

Set は述語なので，それ自体を全要素のリストとして表示することはできません．定義を見たいときは #print，有限範囲で様子を見たいときは Finset.range と filter を組み合わせるとよいです．

def finsetSectionSet : Set Nat :=
  {n | n < 3}

#print finsetSectionSet
#check ((2 : Nat) ∈ finsetSectionSet)

def finsetSectionSetWindow : Finset Nat :=
  (Finset.range 6).filter (fun n => n < 3)

#eval finsetSectionSetWindow

Finset.range n は {0, 1, ..., n - 1} です． decide を #eval すると，具体的な membership の真偽を Bool として見られます．有限和は ∑ i ∈ s, f i の形で書けます．

def finsetSectionRange : Finset Nat :=
  Finset.range 5

#eval finsetSectionRange
#eval decide ((3 : Nat) ∈ finsetSectionRange)
#eval decide ((5 : Nat) ∈ finsetSectionRange)

def finsetSectionRangeSum : Nat :=
  ∑ i ∈ Finset.range 4, i

#eval finsetSectionRangeSum

Fintype α は「型 α 全体が有限である」という型クラスです．たとえば Fin 3 は 3 個の元を持つ型で，Finset.univ はその型の全要素からなる有限集合です． Finset α は「有限個の α の要素を集めたデータ」であり，Fintype α は「型 α 自身が有限である」という構造です．したがって Fintype そのものをデータとして表示するより，その型の全要素を Finset.univ として取り出して表示します．

def finsetSectionFintypeData : Finset (Fin 3) :=
  Finset.univ

#eval finsetSectionFintypeData
#eval Fintype.card (Fin 3)

Subtype は条件を満たす元を「値と証明の組」として持つ型です．表示するときは，元の型への coercion を使うと値の部分を見られます．

def finsetSectionSubtypeElem : ltThreeSubtype :=
  ⟨2, by norm_num [ltThreeSet]⟩

#eval (finsetSectionSubtypeElem : Nat)
#check finsetSectionSubtypeElem.property

Finset と Set は相互に関係しますが，同じものではありません． Finset は有限性をデータとして持つため，和や積を直接定義できます． Set α は単に α → Prop なので，有限とは限らず，有限和には追加の有限性情報が必要です．

演習¶

Finset.range のデータを作り，membership と有限和を #eval で確認してください．

def exerciseRange : Finset Nat :=
  Finset.range 5

#eval exerciseRange
#eval decide ((3 : Nat) ∈ exerciseRange)
#eval decide ((5 : Nat) ∈ exerciseRange)

def exerciseRangeSum : Nat :=
  ∑ i ∈ Finset.range 4, i

#eval exerciseRangeSum

Finset: 有限集合¶

演習¶

`Finset`: 有限集合¶