[Merged by Bors] - chore: avoid some (0 < ((↑) : ℝ≥0 → ℝ) x) = (0 < x) defeq abuses
#41336
Triggered via issue
October 19, 2024 23:14
FR-vdash-bot
Status
Skipped
Total duration
2s
Artifacts
–
labels_from_comment.yml
on: issue_comment
update-label
0s