[Merged by Bors] - doc: Mark named theorems including Compactness Theorem, Halting Problem, Tarski Vaught, Łoś #8743
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
hmonroe
commented
Nov 30, 2023
hmonroe
commented
hmonroe
added
awaiting-review
eric-wieser
approved these changes
Nov 30, 2023
|
✌️ hmonroe can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| @@ -154,8 +154,8 @@ theorem realize_formula_cast {β : Type*} (φ : L.Formula β) (x : β → ∀ a, | |||
| exact congr rfl (Subsingleton.elim _ _) | |||
| #align first_order.language.ultraproduct.realize_formula_cast FirstOrder.Language.Ultraproduct.realize_formula_cast | |||
|
|
|||
| /-- Łoś's Theorem : A sentence is true in an ultraproduct if and only if the set of structures it is | |||
| true in is in the ultrafilter. -/ | |||
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures | |||
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
Suggested change
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures | |
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures |
Comment on lines
157
to
158
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures | ||
| it is true in is in the ultrafilter. -/ |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
Suggested change
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures | |
| it is true in is in the ultrafilter. -/ | |
| /-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures | |
| it is true in is in the ultrafilter. -/ |
|
Long line and trailing spaces are fixed. bors is asking me to approve which may not be correct
|
eric-wieser
reviewed
Nov 30, 2023
Mathlib/Computability/Halting.lean
Outdated
| @@ -230,10 +230,12 @@ theorem rice₂ (C : Set Code) (H : ∀ cf cg, eval cf = eval cg → (cf ∈ C | |||
| exact ⟨by infer_instance, Computable.const _⟩ }⟩ | |||
| #align computable_pred.rice₂ ComputablePred.rice₂ | |||
|
|
|||
| /-- The Halting problem is recursively enumerable */ | |||
There was a problem hiding this comment.
Apologies I should not have applied the Awaiting Review label until checks were complete—I am looking at the checks. I will be making commits from VS Code going forward
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 4, 2023
…em, Tarski Vaught, Łoś (#8743)
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
awueth
pushed a commit
that referenced
this pull request
Dec 19, 2023
…em, Tarski Vaught, Łoś (#8743)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.