Structures · Order
SupSet
Class for the sSup operator
- Defined in
- Mathlib.Order.SetNotation
- Shape
- One type argument · adds sSup
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Every SupSet is also a
Concrete types that are instances39
- Nat
- Real
- EReal
- Tropical
- UpperSet
- LowerSet
- LieSubmodule
- SimpleGraph
- Digraph
- SimpleGraph.Subgraph
- MeasureTheory.OuterMeasure
- SubMulAction
- Seminorm
- ClosedSubmodule
- TwoSidedIdeal
- HomogeneousIdeal
- SimpleGraph.Finsubgraph
- GroupSeminorm
- AddGroupSeminorm
- SubAddAction
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- MeasureTheory.Filtration
- CategoryTheory.Precoverage
- Ideal.Filtration
- Concept
- NonarchAddGroupSeminorm
- Subtype
- Prod
- OrderDual
- ULift
- Lex
- WithTop
- WithBot
- Colex
- Set
- Filter
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by120
- iSup
- SupSet.sSup
- iSup_congr_Prop
- sSup_eq_iSup'
- iSup_apply
- sSup_range
- iSup_of_empty'
- iSup_congr
- Equiv.iSup_comp
- Function.Surjective.iSup_congr
- transfiniteIterate
- sSupHom.comp
- sSup_image'
- iSup_plift_down
- Function.Surjective.iSup_comp
- Equiv.iSup_congr
- sSupHom.id
- iSup_range'
- sSupHom.dual
- WithBot.coe_iSup
- map_iSup
- biSup_congr
- subsetSupSet
- transfiniteIterate_succ
- aeSeq.iSup
- WithTop.coe_iSup
- transfiniteIterate_limit
- WithTop.coe_sSup'
- sSupHom.copy
- sSup_apply
- WithTop.sSup_of_top_mem
- transfiniteIterate_bot
- sSupHom.toFun
- iSup_plift_up
- iSup_ulift
- subset_sSup_of_within
- Equiv.supSet
- map_iSup₂
- biSup_congr'
- sSupHom.comp_apply
- Prod.swap_sSup
- WithTop.sSup_eq
- ULift.down_iSup
- Prod.fst_iSup
- Finset.iSup_coe
- Prod.snd_iSup
- sSupHom.comp_id
- sSupHom.copy_eq
- instCoeTCSSupHomOfSSupHomClass
- Function.Injective.completeBooleanAlgebra