Zulip Chat Archive
Stream: mathlib4
Topic: fin_cases on ordinals
Violeta Hernández (Aug 19 2024 at 00:04):
Out of curiosity. Is there any way to extend the fin_cases tactic to work on say, ordinals or cardinals?
Violeta Hernández (Aug 19 2024 at 00:05):
Specifically, it would work on hypotheses like o ≤ ↑n or o < ↑n, for n : ℕ
Yury G. Kudryashov (Aug 19 2024 at 05:18):
Currently, it needs a locally finite order.
Last updated: May 02 2025 at 03:31 UTC