Theorem ZFSet.coe_subset_coe

Modification history

2026-07-06 15:50
Mathlib/SetTheory/ZFC/Basic.lean
feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet`, `Class` (#32983) …
Modified ZFSet.coe_subset_coeView on Github →
2025-11-21 11:20
Mathlib/SetTheory/ZFC/Basic.lean
refactor(SetTheory/ZFC): deduplicate coercion to sets (#31287) …
Added ZFSet.coe_subset_coeView on Github →