Theorem Cardinal.toNat_monotoneOn

Modification history

2024-02-15 23:16

Mathlib/SetTheory/Cardinal/ToNat.lean

refactor(Cardinal): redefine `toNat` and `toPartENat` (#10472) …

Added Cardinal.toNat_monotoneOn View on Github →