Set: 型の上の集合

Lean は型理論を基礎にしているため，「集合」は型として定義されます． たとえば自然数全体は Nat，実数全体は ℝ という型です． Set α は「型 α の部分集合」の型を表します． 定義は単純で，Set α は α → Prop として実装されています．

Mathlib.Data.Set.Defs

def Set (α : Type u) := α → Prop

つまり，s : Set α とは，各 x : α に対して「x が s に属する」という命題を返す述語です． 所属 x ∈ s は，内部的には s x と同じ意味です． この意味で，Lean の Set α は固定された型 α 上の部分集合全体，つまり冪集合 \(\mathcal P(\alpha)\) に対応します． ただし実際の証明では，Set が関数として実装されていることを直接展開するより，{x | p x} や x ∈ s や s ⊆ t のような集合のインターフェースを使うのが普通です．

対応を大まかに書くと，次のようになります．

• 全体集合・台集合 \(\alpha\): Lean では多くの場合 α : Type*
• 部分集合 \(s \subseteq \alpha\): Lean では s : Set α
• 冪集合 \(\mathcal P(\alpha)\): Lean では Set α という型
• 条件 \(x \in s\): Lean では命題 x ∈ s または s x

Set の notation の定義を読む

Set の記法は，主に次の定義に対応します． x ∈ s は Set.Mem s x，つまり s x です． {x | p x} は述語 p から集合を作る setOf の記法です． s ⊆ t は，s の任意の元が t にも入るという命題です．

Mathlib/Data/Set/Defs.lean

def Set (α : Type u) := α → Prop

def setOf {α : Type u} (p : α → Prop) : Set α :=
  p

namespace Set

protected def Mem (s : Set α) (a : α) : Prop :=
  s a

instance : Membership α (Set α) :=
  ⟨Set.Mem⟩

protected def Subset (s₁ s₂ : Set α) :=
  ∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂

instance : LE (Set α) :=
  ⟨Set.Subset⟩

instance : HasSubset (Set α) :=
  ⟨(· ≤ ·)⟩

#check Set
#check Set.powerset
#check Set.ext
#check Set.mem_setOf
#check Set.setOf_bijective

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

example (n : Nat) : n ∈ ltThreeSet ↔ n < 3 := by
  rfl

example : 2 ∈ ltThreeSet := by
  norm_num [ltThreeSet]

example : 4 ∉ ltThreeSet := by
  norm_num [ltThreeSet]

example (s t : Set Nat) : t ∈ Set.powerset s ↔ t ⊆ s := by
  exact Set.mem_powerset_iff t s

集合の等式は，通常，外延性で証明します． 数学で「任意の x について x ∈ A と x ∈ B が同値だから A = B」と言う議論に対応するのが Set.ext や tactic の ext です．

example (A B : Set Nat) : A ∩ B = B ∩ A := by
  ext x
  simp [and_comm]

Set α と似て見えるものに Subtype があります． s : Set α は α 上の述語であり，それ自体は Set α 型の項です． 一方，{x : α // x ∈ s} は，s に属する元だけを集めた新しい型です． 要素は値 x : α と証明 x ∈ s の組です．

Mathlib では s : Set α を型として使うと，この subtype へ coercion されます． たとえば x : ltThreeSubtype は「ltThreeSet の元」としてのデータであり，(x : Nat) に戻すと元の自然数が得られます．

abbrev ltThreeSubtype : Type :=
  {n : Nat // n ∈ ltThreeSet}

#check Subtype
#check Set.coe_eq_subtype
#check Subtype.mem

example : (⟨2, by norm_num [ltThreeSet]⟩ : ltThreeSubtype).1 = 2 := by
  rfl

example (x : ltThreeSubtype) : (x : Nat) ∈ ltThreeSet := by
  exact x.property

演習

Set が部分集合として振る舞うことを，membership と外延性で確認してください．

example (n : Nat) : n ∈ ltThreeSet ↔ n < 3 := by
  -- 解答例:
  --   rfl
  sorry

example (s t : Set Nat) : t ∈ Set.powerset s ↔ t ⊆ s := by
  -- 解答例:
  --   exact Set.mem_powerset_iff t s
  sorry

Set.ext を使って集合の等式を証明してください．

example {α : Type} (s t : Set α) : s ∩ t = t ∩ s := by
  -- `ext x`, `constructor`, `intro h` で進める．
  -- 解答例:
  --   ext x
  --   constructor
  --   · intro h
  --     exact ⟨h.2, h.1⟩
  --   · intro h
  --     exact ⟨h.2, h.1⟩
  sorry