Structures · Lean core
LE
LE α is the typeclass which supports the notation x ≤ y where x y : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- BitVec
- ENNReal
- Filter.Germ
- UInt64
- UInt8
- UInt16
- UInt32
- NonemptyInterval
- USize
- ENat
- MeasureTheory.SimpleFunc
- Finsupp
- Zsqrtd
- ZNum
- Localization
- Interval
- Int32
- Int8
- Int64
- Int16
- DFinsupp
- CauSeq
- Tropical
- Cardinal
- ISize
- Num
- SimpleGraph
- SignType
- Digraph
- Char
- String
- WithTopology
- RingCon
- ValuativeRel.ValueGroupWithZero
- ValuationRing.ValueGroup
- PosNum
- Function.locallyFinsuppWithin
- String.Pos.Raw
- Finpartition
- Vector
- AddLocalization
- LinearPMap
- Dyadic
- MulArchimedeanOrder
- Class
- ArchimedeanOrder
- Float
- String.Slice.Pos
- String.Pos
- Float32
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- CategoryTheory.GrothendieckTopology
- CategoryTheory.Pretopology
- MeasureTheory.Filtration
- Lean.Grind.Ring.OfSemiring.Q
- MeasurableSpace
- Setoid
- Setoid.Partitions
- Booleanisation
- PSet
- String.Slice
- Semiquot
- SNum
- Std.Time.Month.Offset
- Std.Time.Week.Offset
- Std.Time.Second.Offset
- Std.Time.Minute.Offset
- Std.Time.Nanosecond.Offset
- Std.Time.Day.Offset
- Std.Time.Hour.Offset
- Float32.Model
- Float.Model
- Lean.Grind.IntModule.OfNatModule.Q
- Std.Time.Internal.UnitVal
- TopHom
- BotHom
- Std.Time.Millisecond.Offset
- BoxIntegral.Box
- Std.Time.Year.Offset
- Std.Time.Duration
- BoxIntegral.Prepartition
- Aesop.Percent
- Std.Do.PredTrans
- DivisibleHull
- Std.Time.Timestamp
- Std.Time.WallTime
- Aesop.Nanos
- ManyOneDegree
- Lean.Lsp.Position
- PseudoMetric
- Aesop.SlotIndex
- IO.TaskState
- Lean.Lsp.Range
How is a type an instance?
Loading the hierarchy index…
Assumed by1,726
- OrderIso
- AddLeftMono
- BddAbove
- OrderEmbedding
- OrderIso.symm
- le_top
- MulLeftMono
- BddBelow
- Filter.EventuallyLE
- zero_le
- IsMax
- AddRightMono
- LE.le.trans_eq
- zero_le_one
- IsDirectedOrder
- bot_le
- IsLUB
- IsMin
- upperBounds
- MulRightMono
- IsGLB
- lowerBounds
- Maximal
- IsLowerSet
- sub_nonneg
- Eq.trans_le
- Minimal
- IsUpperSet
- IsLeast
- IsGreatest
- IsCodirectedOrder
- AddLECancellable
- IsCofinal
- IsTop
- IsBot
- Interval
- WithBot.coe_le_coe
- SetLike.le_def
- Filter.isBounded_le_of_top
- IsStrictlyPositive
- le_add_of_nonneg_right
- le_self_add
- WithTop.coe_le_coe
- Convexity.StdSimplex.weights
- MeasureTheory.Submartingale
- NonemptyInterval.toProd
- neg_nonneg
- Filter.isCobounded_le_of_bot
- neg_le_neg_iff
- Filter.isBounded_ge_of_bot
Ancestors0
No ancestors.