Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Add mathlib4 porting warnings

[Merged by Bors] - feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods #7362

Sign in to view logs

[Merged by Bors] - feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods

[Merged by Bors] - feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods #7362

Triggered via pull request September 18, 2023 15:31
@YaelDilliesYaelDillies
synchronize #18629
bounded_le_nhds_class
Status Success
Total duration 36s
Artifacts –

add_ported_warnings.yml

on: pull_request
Check for modifications to ported files
26s
Check for modifications to ported files
Fit to window
Zoom out
Zoom in

Annotations

2 warnings
Check for modifications to ported files: src/order/filter/pi.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/topology/algebra/order/liminf_limsup.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.