doc(Computability/Halting): Mark named theorems (#8577)

Mark these named theorems: Rice, Downward and Upward Skolem
leanprover-community · Nov 25, 2023 · 4b97b73 · 4b97b73
1 parent a538c32
commit 4b97b73
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean
@@ -194,6 +194,7 @@ theorem to_re {p : α → Prop} (hp : ComputablePred p) : RePred p := by
   cases a; cases f n <;> simp
 #align computable_pred.to_re ComputablePred.to_re
 
+/-- **Rice's Theorem** -/
 theorem rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => eval c ∈ C) {f g} (hf : Nat.Partrec f)
     (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C := by
   cases' h with _ h; skip

diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
@@ -504,7 +504,7 @@ instance Tape.inhabited {Γ} [Inhabited Γ] : Inhabited (Tape Γ) :=
   ⟨by constructor <;> apply default⟩
 #align turing.tape.inhabited Turing.Tape.inhabited
 
-/-- A direction for the turing machine `move` command, either
+/-- A direction for the Turing machine `move` command, either
   left or right. -/
 inductive Dir
   | left
@@ -986,7 +986,7 @@ theorem tr_eval' {σ₁ σ₂} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ →
 /-!
 ## The TM0 model
 
-A TM0 turing machine is essentially a Post-Turing machine, adapted for type theory.
+A TM0 Turing machine is essentially a Post-Turing machine, adapted for type theory.
 
 A Post-Turing machine with symbol type `Γ` and label type `Λ` is a function
 `Λ → Γ → Option (Λ × Stmt)`, where a `Stmt` can be either `move left`, `move right` or `write a`
@@ -1349,7 +1349,7 @@ theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt₁} (h : q
   case halt => subst h; trivial
 #align turing.TM1.stmts₁_supports_stmt_mono Turing.TM1.stmts₁_supportsStmt_mono
 
-/-- The set of all statements in a turing machine, plus one extra value `none` representing the
+/-- The set of all statements in a Turing machine, plus one extra value `none` representing the
 halt state. This is used in the TM1 to TM0 reduction. -/
 noncomputable def stmts (M : Λ → Stmt₁) (S : Finset Λ) : Finset (Option Stmt₁) :=
   Finset.insertNone (S.biUnion fun q ↦ stmts₁ (M q))

diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean
@@ -228,8 +228,8 @@ section
 -- Porting note: This instance interrupts synthesizing instances.
 attribute [-instance] FirstOrder.Language.withConstants_expansion
 
-/-- The Upward Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the cardinalities of `L`
-and an infinite `L`-structure `M`, then `M` has an elementary extension of cardinality `κ`. -/
+/-- The **Upward Löwenheim–Skolem Theorem**: If `κ` is a cardinal greater than the cardinalities of
+`L` and an infinite `L`-structure `M`, then `M` has an elementary extension of cardinality `κ`. -/
 theorem exists_elementaryEmbedding_card_eq_of_ge (M : Type w') [L.Structure M] [iM : Infinite M]
     (κ : Cardinal.{w}) (h1 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ)
     (h2 : Cardinal.lift.{w} #M ≤ Cardinal.lift.{w'} κ) :

diff --git a/Mathlib/ModelTheory/Skolem.lean b/Mathlib/ModelTheory/Skolem.lean
@@ -124,7 +124,7 @@ theorem exists_small_elementarySubstructure : ∃ S : L.ElementarySubstructure M
 
 variable {M}
 
-/-- The Downward Löwenheim–Skolem theorem :
+/-- The **Downward Löwenheim–Skolem theorem** :
   If `s` is a set in an `L`-structure `M` and `κ` an infinite cardinal such that
   `max (#s, L.card) ≤ κ` and `κ ≤ # M`, then `M` has an elementary substructure containing `s` of
   cardinality `κ`.  -/