[Merged by Bors] - feat: port CategoryTheory.Subobject.Basic #3444
Conversation
joelriou
commented
Apr 15, 2023
•
joelriou
commented
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
joelriou
added
WIP
joelriou
added
the
awaiting-review
Co-authored-by: Scott Morrison <scott@tqft.net>
| -- it is possible to see its source and target | ||
| -- (`h` will just display as `_`, because it is in `Prop`). | ||
| /-- An inequality of subobjects is witnessed by some morphism between the corresponding objects. -/ | ||
| def ofLe {B : C} (X Y : Subobject B) (h : X ≤ Y) : (X : C) ⟶ (Y : C) := |
There was a problem hiding this comment.
| def ofLe {B : C} (X Y : Subobject B) (h : X ≤ Y) : (X : C) ⟶ (Y : C) := | |
| def ofLe {B : C} (X Y : Subobject B) (h : X ≤ Y) : (X : C) ⟶ (Y : C) := |
I think we have decided to keep LE capitalised even when it is part of a camelCase identifier, although this is fair from uniformly followed. I asked at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/350418574 for clarification on the consensus here.
I'll delegate this PR shortly, feel free to merge either with or without addressing this --- it's a widespread enough inconsistency there's no need to hold up this one in particular.
There was a problem hiding this comment.
Indeed, I was not sure. I shall change Le to LE later today.
|
bors d+ |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors r+ |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
