Theorem ZFSet.not_subset_of_mem

Modification history

2024-12-15 00:11

Mathlib/SetTheory/ZFC/Basic.lean

feat(SetTheory/ZFC/Basic): `x ∈ y → ¬ y ⊆ x` (#19967)

Added ZFSet.not_subset_of_mem View on Github →