LEAN写経　応用情報数理学特論　第１１回

千葉大学 萩原先生の 応用情報数理学特論　第１１回 の演習をLean4で写経してみる．

演習11-01

-- 目標１．data.set
-- 目標２．関数と集合
-- 目標３．型上のinjectiveとsurjective
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
variable {X Y : Type} (S : Set X) (P : X → Prop)

#check ∀ x ∈ S, P x
#check ∃ x ∈ S, P x
example (h : ∀ x ∈ S, P x) (x : X) (h1 : x ∈ S) : P x := h x h1

open Set Function

def maps_to (f : X → Y) (A : Set X) (B : Set Y) : Prop := ∀ x ∈ A, f x ∈ B
def inj_on (f : X → Y) (A : Set X) : Prop := ∀ {x1 x2}, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2
#print inj_on
#print Injective
def surj_on (f : X → Y) (A : Set X) (B : Set Y) : Prop := ∀ y ∈ B, ∃ x ∈ A, f x = y
#print surj_on
#print Surjective

example (g : X → Y) (h1 : Injective g) : inj_on g S := by
  intro x y hx hy hg
  exact h1 hg

-- これは解けない．inj_on は集合 S 以外の単射について言明していないため．
example (g : X → Y) (h1 : inj_on g S) : Injective g := by
  intro x y h1
  sorry

演習11-02

-- 目標１．ext ... (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b 外延性公理
-- 目標２．image f A ... f '' A
-- 目標３．y ∈ f '' A ... ∃ x, x ∈ A ∧ f x = y
import Mathlib.Tactic
open Set Function
variable {X Y : Type}
variable (f : X → Y) (A : Set X) (B : Set Y)

-- 外延性(extensionality)とは，同じ要素をもつ集合は等しいという公理．
theorem image_union (A₁ A₂ : Set X) : image f (A₁ ∪ A₂) = f '' A₁ ∪ f '' A₂ := by
  ext y
  constructor
  -- 方向 → の証明
  · intro h1
    apply Exists.elim h1
    intro a h2
    have hA1A2 : a ∈ A₁ ∨ a ∈ A₂ := h2.left
    have hfa : f a = y := h2.right
    apply Or.elim hA1A2
    · intro hA1
      apply Or.inl -- A₁ の像に入っていることを証明する
      apply Exists.intro a
      apply And.intro hA1 hfa
    · intro hA2
      apply Or.inr -- A₂ の像に入っていることを証明する
      apply Exists.intro a
      apply And.intro hA2 hfa
  -- 方向 ← の証明
  · intro h1
    apply Or.elim h1
    · intro h2
      apply Exists.elim h2
      intro a h3
      apply Exists.intro a
      apply And.intro
      · apply Or.inl
        apply h3.left
      · apply h3.right
    · intro h2
      apply Exists.elim h2
      intro a h3
      apply Exists.intro a
      apply And.intro
      · apply Or.inr
        apply h3.left
      · apply h3.right

演習11-03

-- 目標１．写像になれる
import Mathlib.Tactic
open Set Function

variable {X Y Z: Type}
variable (f : X → Y) (g : Y → Z)

example (A₁ A₂ : Set X) : A₁ ⊆ A₂ → f '' A₁ ⊆ f '' A₂ := by
  intro (h1 : A₁ ⊆ A₂)
  intro (y : Y)
  intro (hyf1 : y ∈ image f A₁)
  apply Exists.elim hyf1
  intro (x : X) (h2 : x ∈ A₁ ∧ f x = y)
  have hxA1 : x ∈ A₁ := h2.left
  have hfxy : f x = y := h2.right
  have hxA2 : x ∈ A₂ := h1 hxA1 -- hxA1 h1 だとエラー h1 は A₁ → A₂ みたいな関数とみなせるのかな
  apply Exists.intro x
  apply And.intro hxA2 hfxy

def surj_on (X₁ X₂ : Type) (g : X₁ → X₂) (A : Set X₁) (B : Set X₂) := B ⊆ g '' A

example (A : Set X) (B : Set Y) : surj_on X Y f A B → ∀ b ∈ B, ∃ a ∈ A, f a = b := by
  intro h y hyB
  have hbfa : B ⊆ f '' A := h
  have hyfa : y ∈ f '' A := hbfa hyB
  apply Exists.elim hyfa
  intro x (h1 : x ∈ A ∧ f x = y)
  apply Exists.intro x
  exact h1