[Merged by Bors] - chore(order/filter/lift): prove has_basis.lift and has_basis.lift'#3618
[Merged by Bors] - chore(order/filter/lift): prove has_basis.lift and has_basis.lift'#3618
has_basis.lift and has_basis.lift'#3618Conversation
has_basis.lift and has_basis.lift' deps: 3611has_basis.lift and has_basis.lift'
src/order/filter/lift.lean
Outdated
| variables {f f₁ f₂ : filter α} {g g₁ g₂ : set α → filter β} | ||
|
|
||
| /-- If `{s i | p i, i : ι}` is a basis of a filter `f`, `g` is a monotone function | ||
| `set α → filter γ`, and for each `i`, `{sg x | pg x, x : β i}` is a basis of the filter `g (s i)`, |
There was a problem hiding this comment.
Is {sg x | pg x, x : β i} now valid syntax? If yes then feel free to merge.
There was a problem hiding this comment.
AFAIK no but I thought that we can use non-valid Lean in comments. If you think otherwise, then I'll try to reformulate.
There was a problem hiding this comment.
I think using non-Lean which looks like Lean is confusing, but I won't insist.
There was a problem hiding this comment.
This notation confused me as well. You may as well use the actually valid version of this, {(s i) | (i : ι) (_ : p i)}, since it's approximately as expressive and doesn't require invented notation.
There was a problem hiding this comment.
I tried to write better docstrings.
|
bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
has_basis.lift and has_basis.lift'has_basis.lift and has_basis.lift'
Deps: #3611