SymmDiff

📁 Source: Mathlib/Data/Finset/SymmDiff.lean

Statistics

Metric	Count
Definitions	0
Theorems coe_symmDiff, image_symmDiff, mem_symmDiff, symmDiff_eq_empty, symmDiff_eq_union, symmDiff_eq_union_iff, symmDiff_nonempty, symmDiff_subset_sdiff, symmDiff_subset_sdiff', symmDiff_subset_union	10
Total	10

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_symmDiff 📖	mathematical	—	SetLike.coe Finset instSetLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff Set GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra Set.instSDiff	—	Set.ext
image_symmDiff 📖	mathematical	—	image symmDiff Finset SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	Set.image_symmDiff
mem_symmDiff 📖	mathematical	—	Finset instMembership symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	—
symmDiff_eq_empty 📖	mathematical	—	symmDiff Finset SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff instEmptyCollection	—	symmDiff_eq_bot
symmDiff_eq_union 📖	mathematical	Disjoint Finset partialOrder instOrderBot	symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff instUnion	—	Disjoint.symmDiff_eq_sup
symmDiff_eq_union_iff 📖	mathematical	—	symmDiff Finset SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff instUnion Disjoint partialOrder instOrderBot	—	symmDiff_eq_sup
symmDiff_nonempty 📖	mathematical	—	Nonempty symmDiff Finset SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	nonempty_iff_ne_empty Iff.not symmDiff_eq_empty
symmDiff_subset_sdiff 📖	mathematical	—	Finset instHasSubset instSDiff symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice	—	subset_union_left
symmDiff_subset_sdiff' 📖	mathematical	—	Finset instHasSubset instSDiff symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice	—	subset_union_right
symmDiff_subset_union 📖	mathematical	—	Finset instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff instUnion	—	symmDiff_le_sup

---

← Back to Index