[Merged by Bors] - chore: tidy various files #7132
Conversation
Ruben-VandeVelde
commented
Sep 13, 2023
Ruben-VandeVelde
commented
Ruben-VandeVelde
added
awaiting-review
| @@ -148,8 +147,9 @@ lemma preconnected_iff_forall_exists_walk_subgraph (H : G.Subgraph) : | |||
| (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩) | |||
|
|
|||
| lemma connected_iff_forall_exists_walk_subgraph (H : G.Subgraph) : | |||
| H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v}, u ∈ H.verts → v ∈ H.verts → | |||
There was a problem hiding this comment.
I kind of preferred the old one, but I think often I don't stick to mathlib style well, so i'll let someone else decide
|
🚀 Pull request has been placed on the maintainer queue by ericrbg. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by ericrbg. |
| @@ -181,7 +181,7 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _). | |||
| topIsAffineOpen _] | |||
| #align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal | |||
|
|
|||
| theorem QuasiCompact.affine_openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) : | |||
| theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) : | |||
There was a problem hiding this comment.
I see that we use both tfae and TFAE... do you know if there is an "official" decision about this?
There was a problem hiding this comment.
Zulip seems to lean towards tfae at the moment, so I'll leave it for now
| @@ -460,7 +460,7 @@ variable [Limits.HasPullbacks C] | |||
| that `f p = g q`, then there is some `s : pullback f g` such that `fst s = p` and `snd s = q`. | |||
|
|
|||
| Remark: Borceux claims that `s` is unique, but this is false. See | |||
| `Counterexamples/Pseudoelement` for details. -/ | |||
| `Counterexamples/Pseudoelement.lean` for details. -/ | |||
There was a problem hiding this comment.
There is no way to make this clickable in the doc, right?
There was a problem hiding this comment.
It's all software, so presumably there is a way. I'd like to look into it at some point, but we'll definitely need a consistent way of referring to file names to make it work. In the mean time, this makes it slightly easier to copy & paste into the "open" dialog or the terminal.
There was a problem hiding this comment.
This works now: leanprover/doc-gen4#151
|
✌️ Ruben-VandeVelde 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
|
bors merge |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
