Theorem ZFSet.toSet_inj

Modification history

2026-05-17 20:27
Mathlib/SetTheory/ZFC/Basic.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted ZFSet.toSet_injView on Github →
2025-11-21 11:20
Mathlib/SetTheory/ZFC/Basic.lean
refactor(SetTheory/ZFC): deduplicate coercion to sets (#31287) …
Modified ZFSet.toSet_injView on Github →
2023-04-06 22:39
Mathlib/SetTheory/Zfc/Basic.lean
feat: port SetTheory.ZFC.Basic (#3165) …
Added ZFSet.toSet_injView on Github →