Structures · Lean core
Min
An overloaded operation to find the lesser of two values of type α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds min
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- ENNReal
- Filter.Germ
- BoundedContinuousFunction
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Units
- MeasureTheory.SimpleFunc
- AddUnits
- Int32
- Int8
- Int64
- Int16
- CauSeq
- FractionalIdeal
- UpperSet
- LowerSet
- MeasureTheory.AEEqFun
- ISize
- LieSubalgebra
- LieSubmodule
- Associates
- SimpleGraph
- CompactlySupportedContinuousMap
- TopologicalSpace.Compacts
- Digraph
- AddSubgroup
- AddSubmonoid
- Sublattice
- BooleanSubalgebra
- UniformSpace
- WithTopology
- SimpleGraph.Subgraph
- Function.locallyFinsuppWithin
- SubMulAction
- TopologicalSpace.OpenNhdsOf
- Seminorm
- Finpartition
- TopologicalSpace.Clopens
- ClosedSubmodule
- HomogeneousIdeal
- SimpleGraph.Finsubgraph
- NonUnitalSubring
- Float
- NonUnitalSubsemiring
- Nucleus
- GroupSeminorm
- AddGroupSeminorm
- SubAddAction
- SaturatedAddSubmonoid
- Float32
- AddSubsemigroup
- SaturatedSubmonoid
- Order.Ideal
- TopologicalSpace.CompactOpens
- StructureGroupoid
- CategoryTheory.Subgroupoid
- FirstOrder.Language.Substructure
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- Projectivization.Subspace
- MeasureTheory.Filtration
- FirstOrder.Language.DefinableSet
- CategoryTheory.Precoverage
- Ideal.Filtration
- GroupTopology
- AddGroupTopology
- Concept
- OpenSubgroup
- OpenAddSubgroup
- Heyting.Regular
- Setoid
- Booleanisation
- OpenNormalAddSubgroup
- OpenNormalSubgroup
- FiniteIndexNormalSubgroup
- FiniteIndexNormalAddSubgroup
- ClosedSubgroup
- Complementeds
- ClosedAddSubgroup
- FiniteGaloisIntermediateField
- ClopenUpperSet
- Subrepresentation
- YoungDiagram
- Float32.Model
- Float.Model
- DiscreteQuotient
- TopHom
- BotHom
- InfHom
- InfTopHom
- Geometry.SimplicialComplex
How is a type an instance?
Loading the hierarchy index…
Assumed by168
- bihimp
- InfHom.toFun
- InfHom.comp
- InfTopHom.comp
- InfTopHom.id
- InfHom.id
- InfTopHom.toInfHom
- InfHom.dual
- InfTopHom.dual
- Filter.Tendsto.inf_nhds'
- MeasureTheory.StronglyMeasurable.inf
- Measurable.inf
- Pi.inf_apply
- AEMeasurable.inf
- InfHom.copy
- InfTopHom.copy
- continuous_inf
- ContinuousWithinAt.inf'
- InfHom.const
- Filter.Tendsto.inf_nhds
- Filter.EventuallyEq.inf
- Continuous.inf
- InfHom.comp_apply
- InfTopHom.toTopHom
- ContinuousAt.inf'
- SemilatticeInf.mk'
- InfTopHom.comp_apply
- Equiv.min
- ContinuousOn.inf'
- Measurable.inf_const
- Function.Injective.distribLattice
- InfTopHom.coe_top
- InfTopHom.instMin
- semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder
- InfHom.instMin
- Function.Injective.linearOrder
- Function.Injective.generalizedHeytingAlgebra
- InfTopHom.coe_toTopHom
- Function.Injective.completeBooleanAlgebra
- InfHom.inf_apply
- ContinuousInf.measurableInf
- InfHom.dual_apply_toFun
- OrderDual.instMeasurableSup₂
- AEMeasurable.inf_const
- Pi.inf_def
- ContinuousAt.inf
- Function.Injective.heytingAlgebra
- InfHom.coe_top
- InfHom.instPartialOrder
- Function.Injective.booleanAlgebra
Ancestors0
No ancestors.