Structures · Lean core
SDiff
Notation type class for the set difference \.
- Defined in
- Init.Core
- Shape
- One type argument · adds sdiff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances38
- SimpleGraph
- Digraph
- Part
- TopologicalSpace.Clopens
- SimpleGraph.Finsubgraph
- Class
- TopologicalSpace.CompactOpens
- ZFSet
- FirstOrder.Language.DefinableSet
- Booleanisation
- Std.TreeMap.Raw
- Std.TreeMap
- Std.DTreeMap
- Std.TreeSet
- Std.DTreeMap.Raw
- Std.TreeSet.Raw
- Std.HashMap
- Std.ExtTreeMap
- Std.HashMap.Raw
- Std.ExtHashMap
- Std.HashSet
- Std.DHashMap.Raw
- Std.DHashMap
- Std.ExtDTreeMap
- Std.HashSet.Raw
- Std.ExtTreeSet
- Std.ExtDHashMap
- Std.ExtHashSet
- RBTree.RBSet
- Lean.NameSet
- Finmap
- Subtype
- Prod
- ULift
- List
- Set
- Finset
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- symmDiff
- symmDiff_def
- Equiv.sdiff
- Part.left_dom_of_sdiff_dom
- Part.right_dom_of_sdiff_dom
- snd_sdiff
- Part.sdiff_mem_sdiff
- Function.Injective.completeBooleanAlgebra
- Part.sdiff_def
- Pi.sdiff_def
- Function.Injective.booleanAlgebra
- Function.Injective.generalizedCoheytingAlgebra
- Function.Injective.completelyDistribLattice
- fst_sdiff
- Part.some_sdiff_some
- Function.Injective.completeAtomicBooleanAlgebra
- Prod.instSDiff
- ULift.instSDiff_mathlib
- Pi.instSDiff
- Equiv.sdiff_def
- Function.Injective.coframe
- Function.Injective.biheytingAlgebra
- Pi.sdiff_apply
- Function.Injective.completeDistribLattice
- Part.sdiff_get_eq
- Function.Injective.coheytingAlgebra
- Part.instSDiff
- ULift.down_sdiff
- ULift.up_sdiff
- Function.Injective.generalizedBooleanAlgebra
Ancestors0
No ancestors.