Structures · Lean core
Sub
The homogeneous version of HSub: a - b : α where a b : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds sub
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Every Sub is also a
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- Quiver.Hom
- Complex
- SeparationQuotient
- NNReal
- BitVec
- ContinuousLinearMap
- ENNReal
- Polynomial
- Filter.Germ
- BoundedContinuousFunction
- Padic
- CStarMatrix
- RatFunc
- UniformSpace.Completion
- UInt64
- NNRat
- UInt8
- UInt16
- UInt32
- Unitization
- Matrix
- WithVal
- HahnSeries
- NonemptyInterval
- LocallyConstant
- USize
- ENat
- QuadraticAlgebra
- MeasureTheory.SimpleFunc
- RestrictedProduct
- TrivSqZeroExt
- Finsupp
- UniformFun
- DoubleCentralizer
- UniformOnFun
- SymAlg
- Interval
- AddUnits
- ContinuousMapZero
- CauSeq.Completion.Cauchy
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- Int32
- Int8
- Int64
- ContinuousAlternatingMap
- Int16
- DFinsupp
- WittVector
- PNat
- CauSeq
- TruncatedWittVector
- WithCStarModule
- Ordinal
- AdicCompletion
- UpperSet
- LowerSet
- MeasureTheory.AEEqFun
- ISize
- Representation.IntertwiningMap
- Language
- AdicCompletion.AdicCauchySequence
- RingCon.Quotient
- Num
- HomogeneousLocalization
- RingQuot
- CentroidHom
- Poly
- ContinuousMultilinearMap
- CompactlySupportedContinuousMap
- MeasureTheory.Measure
- SchwartzMap
- MeasureTheory.VectorMeasure
- Hamming
- AlternatingMap
- IncidenceAlgebra
- AddMonoidHom
- ContinuousAffineMap
- DMatrix
- NormedAddGroupHom
- ZeroHom
- TestFunction
- ContDiffMapSupportedIn
- PosNum
- Function.locallyFinsuppWithin
- Derivation
- AffineMap
- Part
- LieDerivation
- LeftInvariantDerivation
- ModularForm
- SlashInvariantForm
- CuspForm
- PrimeMultiset
- QuadraticMap
How is a type an instance?
Loading the hierarchy index…
Assumed by671
- add_tsub_cancel_right
- tsub_self
- Set.sub
- tsub_zero
- tsub_add_cancel_of_le
- zero_tsub
- add_tsub_cancel_of_le
- Filter.Tendsto.sub
- MeasureTheory.convolution
- Order.pred_eq_sub_one
- Finset.sub
- Continuous.fun_sub
- tsub_le_iff_right
- add_tsub_cancel_left
- tsub_le_iff_left
- tsub_eq_zero_iff_le
- tsub_pos_of_lt
- Matrix.circulant
- tsub_pos_iff_lt
- tsub_eq_zero_of_le
- Pi.sub_apply
- Continuous.sub
- tsub_add_eq_add_tsub
- tsub_le_self
- ContinuousOn.sub
- Filter.EventuallyEq.sub
- ContinuousAt.fun_sub
- MeasureTheory.ConvolutionExistsAt
- MeasureTheory.StronglyMeasurable.sub
- ContinuousOn.fun_sub
- tsub_le_tsub
- tsub_le_tsub_right
- add_tsub_assoc_of_le
- lt_tsub_iff_right
- Filter.Tendsto.const_sub
- Filter.Tendsto.sub_const
- tsub_le_tsub_left
- FunLike.coe_sub
- Measurable.sub
- le_add_tsub
- Measurable.const_sub
- tsub_mul
- tsub_eq_iff_eq_add_of_le
- ProbabilityTheory.HasIndepIncrements
- mul_tsub
- le_tsub_of_add_le_left
- AddLECancellable.tsub_eq_of_eq_add
- eq_tsub_of_add_eq
- le_tsub_add
- tsub_tsub_cancel_of_le