第4部 数学の基本言語

問題1集合演算を論理式へ翻訳する

Problem

問題

Subset s t と Intersection s (Union t u) x を、集合記号を使わない量化・含意・連言・選言の式へ翻訳せよ。次に積集合の交換性を連言の交換から証明し、集合の証明が要素を固定した命題の証明へ還元される順序を示す。

同じ方法で Subset (Singleton x) s ↔ s x をLeanで証明する。数式中の各推論が、関数適用、等式による書換え、含意のどれとして現れるかを対応づけること。

ヒント

集合 A を所属述語 x ↦ x∈A と読み、演算を論理結合子へ一つずつ移します。

解答

x∈A∩B ↔ x∈A ∧ x∈B、x∈A∪B ↔ x∈A ∨ x∈B、x∈Aᶜ ↔ ¬x∈A です。包含は A⊆B ↔ ∀x, x∈A→x∈B、差は x∈A\B ↔ x∈A∧¬x∈B、像は y∈f '' A ↔ ∃x, x∈A∧f x=y、逆像は x∈f ⁻¹' B ↔ f x∈B になります。集合等式は外延性によりすべてのxについて所属が同値であることへ還元されます。

添字付き和と共通部分は存在量化と全称量化へ翻訳でき、極限に現れる集合族の記法も読めます。

Lean検査済みL297–305

open FormalLab.Mathematics.Sets

theorem singletonSubset {α : Type} {chosen : α} {set : PredSet α} :
    Subset (Singleton chosen) set ↔ set chosen := by
  constructor
  · intro included
    exact included rfl
  · intro member x equal
    exact equal.symm ▸ member

問題2外延性が重ねて使われる箇所を追う

Problem

問題

二つの述語 s t : α → Prop が同じ集合を表すための条件を述べ、関数外延性と命題外延性をどの順に使えば s = t が得られるかを導出せよ。要素ごとの同値、命題の等式、関数の等式を混同せず、三段階に分けて書くこと。

Leanの集合が述語として表現されることから従う実装上の説明と、数学における集合外延性の原理を区別する。どの段階がLeanの表現選択に依存するかを指摘できれば完了である。

ヒント

関数値が集合である等式では、関数外延性と集合外延性を順に適用します。

解答

例えば f ⁻¹' (B∩C) = f ⁻¹' B ∩ f ⁻¹' C は集合外延性で任意のxの所属同値へ移り、定義展開だけで f x∈B∧C ↔ f x∈B∧f x∈C となります。一方、写像 preimage f : Set Y→Set X 同士の等式を示すなら、まず関数外延性で任意のBを固定し、次に集合外延性で任意のxを固定します。二つの外延性は異なる型の等号を一層ずつ観察可能な値へ下ろします。

自然変換の等号でも成分ごとの外延性、さらに関数や集合の外延性という層を順に下ります。

Lean検査済みL311–314

theorem predicateExtensionality {α : Type} {left right : α → Prop}
    (pointwise : ∀ x, left x ↔ right x) : left = right := by
  funext x
  exact propext (pointwise x)

問題3補集合と古典論理の境目を特定する

Problem

問題

s ∪ sᶜ = Universal の通常の証明を要素ごとの命題へ展開し、排中律を用いる正確な一行を指せ。一方、s ∩ sᶜ = Empty は同じ古典原理なしに証明できることを示し、否定の導入と排中律の違いを説明する。

最後に、構成的に証明できる包含関係と、古典論理を仮定して初めて等号まで強められる関係を一つずつ挙げる。古典性を集合記号の見かけではなく、対応する論理式から判定すること。

ヒント

補集合の定義自体と、二重否定除去や排中律を必要とする等式を区別します。

解答

Aᶜ={x|¬x∈A} は構成的に定義できます。A∩Aᶜ=∅ と A⊆(Aᶜ)ᶜ も矛盾導出だけで証明できます。逆包含 (Aᶜ)ᶜ⊆A は各xについて ¬¬(x∈A)→x∈A を要求し、一般には古典論理が必要です。同様に A∪Aᶜ=U は所属命題についての排中律です。有限で所属が決定可能な集合なら、その決定手続きから局所的に証明できます。

位相の閉包や論理の否定を扱うときも、古典的同値を無意識に使わず方向ごとの構成可能性を調べます。

Lean検査済みL320–338

open FormalLab.Mathematics.Sets

theorem intersectionComplement {α : Type} (set : PredSet α) :
    Intersection set (Complement set) = FormalLab.Mathematics.Sets.Empty := by
  funext x
  apply propext
  constructor
  · exact fun ⟨member, notMember⟩ => notMember member
  · exact False.elim

theorem unionComplement {α : Type} (set : PredSet α) :
    Union set (Complement set) = Universal := by
  classical
  funext x
  apply propext
  constructor
  · exact fun _ => trivial
  · intro _
    exact Classical.em (set x)

第21章

数学的関数とその性質

問題1左逆から単射を復元する

Problem

問題

関数 f : α → β と g : β → α について、左逆と右逆の式を合成の順序まで含めて数式で書け。次に leftInverseGivesInjective の等式列を一行ずつ展開し、各行が合同性、左逆の仮定、与えられた等式のどれを使うか注記せよ。

最後に、全単射な f と、f の左逆かつ右逆である g から IsBijective g をLeanで証明する。単射と全射の証明で左右どちらの逆の式を使ったかを説明できれば完了である。

ヒント

g∘f=id と f x=f y をgで写します。

解答

f:A→B と g:B→A が ∀x, g(f x)=x を満たすとします。f x=f y なら合同性から g(f x)=g(f y) です。左逆の等式を両辺へ用いて x=y を得るのでfは単射です。逆に単射だけから B全体上の左逆を作るには、像の外の値へ送るAの要素が必要です。Aが空でBが非空なら単射は存在しても B→A は存在しません。

右逆から全射を得る双対的証明を書き、逆向きで選択が必要になる条件も比較します。

Lean検査済みL344–356

open FormalLab.Mathematics.FunctionProperties

theorem inverseIsBijective {α β : Type} {f : α → β} {g : β → α}
    (left : IsLeftInverse g f) (right : IsRightInverse g f) : IsBijective g where
  injective := by
    intro x y equal
    calc
      x = f (g x) := (right x).symm
      _ = f (g y) := congrArg f equal
      _ = y := right y
  surjective := by
    intro x
    exact ⟨f x, left x⟩

問題2像と逆像の量化を比較する

Problem

問題

Image f s y と Preimage f t x を論理結合子と量化記号だけで展開せよ。前者では始域の要素を存在量化するのに、後者では f x を直接検査できる理由を、型の情報の流れとして説明する。具体例として f n = n % 2 を用い、単集合の像と逆像を一つずつ計算せよ。

同じ式で定めた関数でも終域を変えると全射性が変わる例を作り、全射性が値の計算だけでなく始域・終域を含む関数の型の性質であることを確認せよ。

ヒント

像には原像の証人が必要ですが、逆像は関数適用だけで判定できます。

解答

y∈f '' A は ∃x, x∈A∧f x=y という存在命題です。x∈f ⁻¹' B は単に f x∈B です。この差から逆像は共通部分と和の両方を厳密に保存します。像は和を厳密に保存しますが、共通部分について一般には f '' (A∩C) ⊆ f '' A∩f '' C だけです。逆包含には、右辺の二つの存在証人を同じにするためfの単射が使えます。

随伴する像と逆像の包含 f '' A⊆B ↔ A⊆f ⁻¹'B を量化の変形だけで導きます。

Lean検査済みL362–372

open FormalLab.Mathematics.FunctionProperties
open FormalLab.Mathematics.Sets

def parity (n : Nat) : Nat := n % 2

example : Image parity (Singleton 3) 1 := by
  exact ⟨3, rfl, by decide⟩

example : Preimage parity (Singleton 0) 4 := by
  change 4 % 2 = 0
  decide

問題3逆関数を選ぶために必要な仮定を調べる

Problem

問題

単射 f : α → β から左逆 g : β → α を構成しようとすると、像の外の y : β にどの値を返すかが未決定になる。α が空の場合と空でない場合を分け、どの箇所で既定値または選択原理が必要になるかを分析せよ。

「単射なら無条件に計算可能な左逆が得られる」という主張の誤りを、型が空である例を含めて示すこと。定理として証明できる部分と、追加仮定に依存する構成を区別できれば完了である。

ヒント

全射の各値に対する原像の「存在」から、原像を返す一つの「関数」へ移る箇所を見ます。

解答

全射 ∀y,∃x,f x=y から右逆 g:B→A を作るには、各yについて証人xを選びます。依存選択関数 choose : (∀y,∃x,P y x)→∀y,{x // P y x} があれば g y=(choose h y).1 と定義できます。有限型で探索が可能、または各繊維に標準的な代表があれば選択公理は不要です。全単射の場合は単射性により原像は一意ですが、存在から関数を抽出する原理は基礎体系に依存します。

商集合の代表元選択や基底選択でも、存在・一意性・計算可能な選択を別々に記録します。

第22章

関係・同値・順序

問題1対称性と反対称性を反例で分ける

Problem

問題

二つの性質を量化記号を省かずに展開し、仮定と結論を比較せよ。自然数の ≤、等式、空関係、常に真な関係を行とする表を作る。各関係について反射性・対称性・反対称性・推移性の真偽を記し、偽の場合には最小限の具体的反例を添える。

とくに「対称でない」ことと「反対称である」ことが両立する例を説明せよ。名称の類似ではなく、含意の向きと等式が現れる位置から両者を再構成できれば完了である。

ヒント

対称性は矢印を反転し、反対称性は両方向の矢印から頂点の一致を結論します。

解答

整数の等差関係 xRy ↔ x-y が偶数は対称ですが、0と2が両方向に関係しても等しくないため反対称ではありません。自然数の通常の順序≤は反対称ですが、0≤1 に対し 1≤0 は偽なので対称ではありません。等号は両方を満たし、空関係も両条件を空虚に満たします。性質名ではなく量化式を使えば混同を避けられます。

前順序から同値部分 x≤y∧y≤x を商にすると、反対称な半順序が得られる過程を追います。

問題2関数の核関係を証明する

Problem

問題

Kernel f x y :↔ f x = f y から反射性・対称性・推移性を証明し、それぞれが等式のどの法則に由来するか注記せよ。さらに f が単射なら Kernel f x y ↔ x = y をLeanで示し、逆向きには単射を必要としない理由を述べる。

定数関数の核関係も計算し、単射性を失うと異なる入力の区別がどのように消えるか確認する。これにより核が関数によって観測できない差を表すことを、自分の例で説明せよ。

ヒント

x∼y ↔ f x=f y と定義し、等号の三性質を移します。

解答

反射性は f x=f x、対称性は f x=f y の対称、推移性は f x=f y と f y=f z の推移から従います。従って核関係は同値関係です。さらに x∼y ↔ f x=f y なので、fは同値類上で一定です。逆に異なる同値類が同じ像を持てば代表x,yが関係して同じ類になるため、商から像への誘導写像は単射になります。

群準同型の核や型の観察同値を、値ではなく区別不能性を集める同じ構成として比較します。

Lean検査済みL378–392

open FormalLab.Mathematics.FunctionProperties
open FormalLab.Mathematics.Relations

theorem kernelEquivalence {α β : Type} (f : α → β) : IsEquivalence (Kernel f) where
  reflexive := fun _ => rfl
  symmetric := fun _ _ equal => equal.symm
  transitive := fun _ _ _ first second => first.trans second

theorem kernelEqualsEquality {α β : Type} {f : α → β} (injective : IsInjective f)
    (x y : α) : Kernel f x y ↔ x = y := by
  constructor
  · intro sameOutput
    exact injective sameOutput
  · intro equal
    exact congrArg f equal

問題3同値関係から商へ進む理由を説明する

Problem

問題

偶奇が等しいという自然数上の関係を定義し、同値関係であることを確認せよ。しかし、関係が成り立つ二数をLeanの等式で置換してはならない。1 と 3 を使い、その誤った置換が何を壊すか示すこと。

同値関係は「等しいと扱いたい」という規約を与え、商はその規約を新しい等式へ反映する構成である。この二段階を、関係、同値類、代表元不変な関数という三語を用いて説明できれば完了である。

ヒント

同値な代表を同じ対象として扱う操作が代表の選び方に依存しない条件を書きます。

解答

同値関係だけでは元xとyは依然として別の値です。商 A/∼ は同値類を一つの点として扱い、射影 q:A→A/∼ は x∼y を q x=q y へ変えます。関数 f:A→B が同値類上で一定なら、かつそのときに限り f= f̄∘q となる一意な f̄:A/∼→B を定められます。この普遍性が、代表元によらない定義と証明を保証します。

余等化子は「二つの写像が同じになる最小の商」として、商の普遍性を圏論へ一般化します。

第23章

自然数の再帰・場合分け・帰納法

問題1帰納法の四つの役割を分離する

Problem

問題

zeroAdd で証明している述語を P n := ... の形で書き、基底部、帰納仮定、帰納段階、最終的な全称命題を区別せよ。Leanの Nat.rec または帰納法タクティックの各引数が、この数式による構成のどこに対応するかを表にする。

続いて n + 0 = n と 0 + n = n を証明し、片方が定義計算で閉じ、もう片方が帰納法を要する理由を加算の再帰引数から説明せよ。式の左右対称性だけでは証明方法まで対称にならないことを確認できれば完了である。

ヒント

対象の構成、関数の定義、命題の証明、計算規則を別の欄へ置きます。

解答

帰納型宣言は0と後者で自然数を生成します。場合分けは入力が0か後者かを一層だけ観察します。再帰は0での値と、 nおよび再帰結果からn+1での値を与えて関数を定義します。帰納法は命題Pについて P 0 と ∀n,P n→P(n+1) から ∀n,P n を示します。再帰子の計算規則は0と後者で定義がどう簡約するかを定めます。

リストや木でも同じ四分類を使い、データ定義とそれについての証明を混同しないようにします。

Lean検査済みL398–420

theorem addZero (n : Nat) : n + 0 = n := rfl

theorem zeroAdd (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n inductionHypothesis =>
      exact congrArg Nat.succ inductionHypothesis

def triangular : Nat → Nat
  | 0 => 0
  | n + 1 => triangular n + (n + 1)

theorem twiceTriangular (n : Nat) : 2 * triangular n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ n inductionHypothesis =>
      calc
        2 * triangular (n + 1) = 2 * triangular n + 2 * (n + 1) := by
          rw [triangular, Nat.mul_add]
        _ = n * (n + 1) + 2 * (n + 1) := by rw [inductionHypothesis]
        _ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
        _ = (n + 1 + 1) * (n + 1) := by congr 1
        _ = (n + 1) * (n + 1 + 1) := Nat.mul_comm _ _

補足

三角数のような例では、関数を作る段階は再帰、閉じた公式を示す段階は帰納です。後者の場合には再帰方程式で左辺を一段計算し、帰納仮定で小さい入力の結果を置換してから算術を閉じます。induction と自動算術だけを眺めず、どの行が構成、計算、帰納仮定の使用に当たるかを分けると、リストや木にも同じ証明設計を移せます。

問題2再帰計算と帰納証明を同じ構造から読む

Problem

問題

sumTo 3 を定義に従って一段ずつ展開する。その後、 sumTo (n + 1) = sumTo n + (n + 1) をまず定義展開だけで証明し、どの式が判断的に簡約され、どの式が命題的等式として残るかを記録せよ。

zeroOrSuccessor ではなぜ帰納仮定を使わないのかも説明する。構造を一段観察する場合分けと、小さい対象について得た命題を次へ運ぶ帰納法との違いを、Leanコードと推論規則による導出の両方から述べること。

ヒント

加法 add n m の再帰式と、add n 0=n の帰納証明を0・後者の二行で並べます。

解答

第一引数で再帰する加法を add 0 m=m、add (n+1) m=add n m+1 とします。定理 add n 0=n は、0の場合に定義計算で成立します。後者の場合は定義式で add (n+1) 0=add n 0+1 とし、帰納仮定で右辺を n+1 にします。計算では再帰結果を値として使い、証明では同じ小さい入力についての命題を等式書換えとして使います。

証明と計算の融合により、証明付きプログラムや依存消去子が同じ再帰原理から得られることを確認します。

Lean検査済みL426–430

open FormalLab.Mathematics.NaturalNumberInduction

#eval sumTo 3

example (n : Nat) : sumTo (n + 1) = sumTo n + (n + 1) := rfl

出力

問題3別の帰納型へ原理を移す

Problem

問題

要素型 α をもつ自作のリスト型を定義し、長さ関数を構造再帰で実装せよ。さらに、連結した二つのリストの長さが長さの和になることを構造帰納法で証明する。再帰関数の各分岐と帰納証明の各分岐を一対一に対応づけること。

自然数で学んだ構成のうち、0 と後者関数に固有だった部分と、任意の帰納型にも通用する部分を分けて説明できれば、この問題の到達点に達している。

ヒント

二分木の各構成子に対し、証明すべき場合と得られる帰納仮定を一つずつ用意します。

解答

Tree A ::= leaf a | node l r とします。性質Pを全木で示すには、全aについて P(leaf a) を示し、全l,rについて P l と P r から P(node l r) を示します。節点数 size に対する size t≥1 は葉で計算し、節点では二つの帰納仮定と size(node l r)=1+size l+size r を使います。再帰位置が二つなので帰納仮定も二つです。

添字付き帰納族では各構成子が到達できる添字も帰納原理へ現れ、不可能な場合を消去できます。

Lean検査済みL436–454

inductive Sequence (α : Type) where
  | nil
  | cons (head : α) (tail : Sequence α)

def Sequence.append : Sequence α → Sequence α → Sequence α
  | .nil, right => right
  | .cons head tail, right => .cons head (tail.append right)

def Sequence.length : Sequence α → Nat
  | .nil => 0
  | .cons _ tail => tail.length + 1

theorem lengthAppend (left right : Sequence α) :
    (left.append right).length = left.length + right.length := by
  induction left with
  | nil => simp [Sequence.append, Sequence.length]
  | cons head tail inductionHypothesis =>
      simp only [Sequence.append, Sequence.length]
      omega

第24章

順序・上限・下限・極大原理

問題1上限の二条件を別々に検査する

Problem

問題

自然数の有限部分集合を一つ選び、上界を三つ挙げ、そのうち上限だけが満たす追加条件を書いてください。次に空集合と自然数全体について上界・上限の有無を調べます。空虚に成立する量化と、候補となる自然数が存在しない場合を分け、UpperBound と IsSupremum のどちらの成分で失敗するかを示します。

ヒント

上界であることと、すべての上界以下であることを分け、それぞれ片方だけ満たす候補を作ります。

解答

実数集合 S=(0,1) では1は上界で、任意の上界uに対し1≤uなので上限です。2は上界ですが最小ではありません。 0は2以下を含む多くの上界以下ですが、Sの上界ではありません。従って候補sが上限であるには ∀x∈S,x≤s と ∀u,(∀x∈S,x≤u)→s≤u の両方が必要です。第二条件だけを「小さい」と読むと対象集合との接続を失います。

圏論的極限でも錐であることと、任意の錐から一意に因子化することを同じ二段階で検査します。

問題2最大と極大の差を有限半順序で可視化する

Problem

問題

Boundary の四候補をHasse図に描き、各点が極大・最大・最小のどれかを判定してください。別の三要素半順序をLeanで定義し、極大元が二つある例と最大元が一つある例を作ります。偽の判定には比較不能な二点を具体的に挙げ、反対称性の失敗と混同していないことも確認します。最後に、全順序なら有限部分集合の極大元が最大元になることを証明し、どの段階で比較可能性を使ったかを示せば完了です。

ヒント

互いに比較不能な二要素を上端に持つV字型の半順序を使います。

解答

集合 {a,b,c} に a<b、a<c だけを加えます。bより真に大きい元もcより真に大きい元もないため、bとcはともに極大です。しかし最大元mはすべてのxに対し x≤m を満たす必要があり、bとcは比較不能なので存在しません。最大元があれば一意で極大ですが、極大元は複数あり得ます。全順序では比較不能性がないため有限非空集合の極大元は最大元になります。

最適化のPareto最適点は極大であり、単一の最大とは限らないという同じ区別を使います。

Lean検査済みL460–487

open FormalLab.Mathematics.Relations

inductive Fork where
  | bottom
  | left
  | right
  deriving DecidableEq

def ForkLe (first second : Fork) : Prop := first = .bottom ∨ first = second

theorem forkPartialOrder : IsPartialOrder ForkLe where
  reflexive := fun point => Or.inr rfl
  antisymmetric := by
    intro first second forward backward
    rcases forward with atBottom | equal
    · rcases backward with secondBottom | reverse
      · exact atBottom.trans secondBottom.symm
      · exact reverse.symm
    · exact equal
  transitive := by
    intro first second third firstSecond secondThird
    rcases firstSecond with atBottom | equal
    · exact Or.inl atBottom
    · subst second
      exact secondThird

theorem leftAndRightIncomparable : ¬ForkLe .left .right ∧ ¬ForkLe .right .left := by
  simp [ForkLe]

問題3Zornの仮定を有限性で弱めてはならない理由を述べる

Problem

問題

ZornConclusion の各量化を通常の数式へ戻し、空でないこと、鎖、上界、極大元の役割を説明します。有限半順序では極大元を探索できる証明を帰納法で与え、その証明が無限の場合に停止しない箇所を特定します。 [ZOR35] の主張と現代的定式化を比較し、歴史的原文と後世の同値定理を区別してください。

ヒント

有限半順序の極大元証明と、無限鎖を扱うZornの補題で停止根拠が何かを比較します。

解答

有限非空半順序では、極大でない元からより大きい元へ進む操作は有限回で止まり、極大元を得ます。無限半順序ではこの上昇が止まる保証はありません。Zornの補題は有限性の代わりに、すべての鎖が上界を持つと仮定して極大元を結論します。自然数の通常順序は非空で各有限鎖に上界がありますが極大元を持ちません。無限鎖N自体の上界が存在しないため、Zornの「すべての鎖」を「すべての有限鎖」へ弱めることはできません。

基底延長や極大イデアルの存在証明では、対象となる鎖の上界を和集合で構成できることを個別に証明します。

第25章

有限性・可算性・基数・無限

問題1単射・全射・全単射で三種類の比較を作る

Problem

問題

Bool、Nat、EvenNatの各組について単射または全射を具体的に構成し、全単射まで得られる組を判定してください。関数の始域・終域を省略せず、同じ式でも終域を変えると全射性が変わる例を含めます。「部分集合だから小さい」という推論が無限の場合に不十分な理由をtoEvenから説明します。

ヒント

有限集合と自然数、自然数と整数、自然数と実数を例にします。

解答

Fin n→N には単射があるので有限集合の濃度はN以下です。NとZには、0、正、負を交互に並べる全単射があり、無限部分集合でも同じ可算濃度になり得ます。NからRへの単射はありますが全射はありません。Cantorの対角線論法によりRの列挙を仮定すると列挙にない実数を作れるからです。一般に |A|≤|B| はAからBへの単射、等濃度は全単射で定義します。BからAへの全射との同値には空集合や選択の扱いを明記します。

Cantor–Bernstein定理を使えば、両方向の単射から全単射を構成して濃度比較を閉じられます。

Lean検査済みL493–500

open FormalLab.Mathematics.Cardinality
open FormalLab.Mathematics.FunctionProperties

example : IsBijective toEven where
  injective := toEvenInjective
  surjective := by
    intro even
    exact ⟨fromEven even, toEvenFromEven even⟩

問題2対角線証明を表として追跡する

Problem

問題

三行三列の有限な真偽値表を一つ作り、対角成分を反転した列を書いてください。その列が各行と異なる位置を一つずつ示します。次にdiagonalDiffersのcongrFunがこの一点比較へ対応することを説明し、有限表では新しい列が表の列数を越えるだけで、一般定理の論理が有限性に依存しないことを確認します。

ヒント

二進無限列の列挙を仮定し、n行n列目を反転した新しい列を作ります。

解答

s₀,s₁,… : N→Bool が全列の列挙だと仮定します。新しい列dを d(n)=not(sₙ(n)) と定めます。任意のkについて d(k)≠s_k(k) なので、関数外延性の反対方向から d≠s_k です。従ってdはどの行にもなく、列挙の全射性に矛盾します。反転は「列全体と違う」ことを一度に示すのではなく、k番目の候補とk番目の座標で違うことを各kについて保証します。

冪集合定理では d={a∈A | a∉f(a)} と置き、同じ自己参照する対角成分で全射 A→P(A) を否定します。

Lean検査済みL506–511

open FormalLab.Mathematics.Cardinality

def table : Fin 3 → Fin 3 → Bool := fun row column => row = column

example (row : Fin 3) : diagonal table ≠ table row :=
  diagonalDiffers table row

問題3可算性と宇宙を別々の判断へ戻す

Problem

問題

Nat : Type、Type : Type 1、AtMostCountable Natを三つの異なる主張として展開してください。宇宙レベルを一段持ち上げたULift NatとNatの間に全単射を構成し、宇宙が変わっても要素対応が保存される例を示します。[CAN74]の実数非可算性と本章のBool冪型定理の論証形式も比較します。