Theorem Subrel.coe_inclusionEmbedding

Modification history

2025-01-15 15:41
Mathlib/Order/RelIso/Set.lean
refactor: redefine `Subrel` in terms of `α → Prop` instead of `Set α` (#20475) …
Modified Subrel.coe_inclusionEmbeddingView on Github →
2024-12-15 00:44
Mathlib/Order/RelIso/Set.lean
feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals (#17001) …
Added Subrel.coe_inclusionEmbeddingView on Github →