Theorem Subrel.coe_inclusionEmbedding

Modification history

2024-12-15 00:44

Mathlib/Order/RelIso/Set.lean

feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals (#17001) …

Added Subrel.coe_inclusionEmbedding View on Github →