SymmDiff

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

Statistics

Metric	Count
Definitions	0
Theorems inter_symmDiff_distrib_left, inter_symmDiff_distrib_right, mem_symmDiff, subset_symmDiff_union_symmDiff_left, subset_symmDiff_union_symmDiff_right, symmDiff_def, symmDiff_eq_empty, symmDiff_nonempty, symmDiff_subset_union, symmDiff_union_subset, union_symmDiff_subset, union_symmDiff_union_subset	12
Total	12

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_symmDiff_distrib_left 📖	mathematical	—	Set instInter symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff	—	inf_symmDiff_distrib_left
inter_symmDiff_distrib_right 📖	mathematical	—	Set instInter symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff	—	inf_symmDiff_distrib_right
mem_symmDiff 📖	mathematical	—	Set instMembership symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff	—	—
subset_symmDiff_union_symmDiff_left 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	instHasSubset instUnion symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instSDiff	—	Disjoint.le_symmDiff_sup_symmDiff_left
subset_symmDiff_union_symmDiff_right 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	instHasSubset instUnion symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instSDiff	—	Disjoint.le_symmDiff_sup_symmDiff_right
symmDiff_def 📖	mathematical	—	symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instUnion	—	—
symmDiff_eq_empty 📖	mathematical	—	symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instEmptyCollection	—	symmDiff_eq_bot
symmDiff_nonempty 📖	mathematical	—	Nonempty symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff	—	nonempty_iff_ne_empty Iff.not symmDiff_eq_empty
symmDiff_subset_union 📖	mathematical	—	Set instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instUnion	—	symmDiff_le_sup
symmDiff_union_subset 📖	mathematical	—	Set instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instUnion	—	—
union_symmDiff_subset 📖	mathematical	—	Set instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instUnion	—	—
union_symmDiff_union_subset 📖	mathematical	—	Set instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff instUnion	—	—

---

← Back to Index