Theorem Equiv.toEmbedding_injective

Modification history

2024-01-12 06:00
Mathlib/Logic/Embedding/Basic.lean
feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …
Added Equiv.toEmbedding_injectiveView on Github →