Structures · Order
PartialOrder
A partial order is a reflexive, transitive, antisymmetric relation ≤.
- Defined in
- Mathlib.Order.Defs.PartialOrder
- Shape
- One type argument · adds le_antisymm
Extends1
Extended by11
Forgetful instances
Provided automatically by
Concrete types that are instances100
- Nat
- Real
- Rat
- Bool
- NNReal
- ContinuousLinearMap
- ENNReal
- Filter.Germ
- BoundedContinuousFunction
- CStarMatrix
- Unitization
- NonemptyInterval
- Units
- MeasureTheory.SimpleFunc
- EReal
- Finsupp
- Localization
- Interval
- AddUnits
- ContinuousMapZero
- DFinsupp
- SetSemiring
- TopologicalSpace.NonemptyCompacts
- Tropical
- Ordinal
- FractionalIdeal
- UpperSet
- LowerSet
- Cardinal
- MeasureTheory.AEEqFun
- LieSubalgebra
- LieSubmodule
- Num
- AlgebraicGeometry.Scheme.IdealSheafData
- Associates
- PrimeSpectrum
- SimpleGraph
- CompactlySupportedContinuousMap
- MeasureTheory.Measure
- TopologicalSpace.Opens
- MeasureTheory.VectorMeasure
- TopologicalSpace.Compacts
- Digraph
- AddSubgroup
- Sym2
- ProbabilityTheory.Kernel
- AddSubmonoid
- NonUnitalSubalgebra
- NonUnitalStarSubalgebra
- Sublattice
- BooleanSubalgebra
- UniformSpace
- TopologicalSpace
- WithTopology
- TopologicalSpace.Closeds
- RingCon
- SimpleGraph.Subgraph
- MeasureTheory.OuterMeasure
- SubMulAction
- TopologicalSpace.OpenNhdsOf
- Part
- ConvexBody
- Partition
- ConvexCone
- Seminorm
- Finpartition
- StarSubalgebra
- AddLocalization
- Flag
- OrderRingHom
- TopologicalSpace.Clopens
- ClosedSubmodule
- TwoSidedIdeal
- HomogeneousIdeal
- Antisymmetrization
- AffineSubspace
- NonUnitalSubring
- CategoryTheory.Subobject
- Sublocale
- NonUnitalSubsemiring
- Nucleus
- GroupSeminorm
- AddGroupSeminorm
- SubAddAction
- SaturatedAddSubmonoid
- AddSubsemigroup
- SaturatedSubmonoid
- Order.Ideal
- TopologicalSpace.CompactOpens
- ZFSet
- StructureGroupoid
- CategoryTheory.Subgroupoid
- FirstOrder.Language.Substructure
- DividedPowers.SubDPIdeal
- DyckWord
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- Projectivization.Subspace
- CategoryTheory.GrothendieckTopology
- CategoryTheory.Pretopology
How is a type an instance?
Loading the hierarchy index…
Assumed by7,368
- Disjoint
- le_antisymm
- zero_lt_one
- Convex
- LE.le.antisymm
- Orientation
- div_pos
- pow_pos
- Set.PairwiseDisjoint
- Nat.cast_nonneg'
- eq_top_iff
- HahnSeries.coeff
- ConvexOn
- lt_of_le_of_ne
- neg_neg_of_pos
- LE.le.eq_or_lt
- Nat.cast_pos'
- Nat.floor
- Codisjoint
- pos_iff_ne_zero
- top_le_iff
- add_tsub_cancel_right
- Wbtw
- convexHull
- Ne.lt_top
- ConcaveOn
- eq_bot_iff
- Nat.cast_le
- tsub_self
- PointedCone
- subset_antisymm
- SameRay
- lt_of_le_of_ne'
- Nat.ceil
- Disjoint.symm
- inv_pos
- zero_lt_two
- inv_pos_of_pos
- tsub_zero
- Sbtw
- segment
- StrictMono.monotone
- le_bot_iff
- Ne.bot_lt
- LE.le.lt_of_ne
- Nat.cast_pos
- tsub_add_cancel_of_le
- Nat.cast_nonneg
- lt_add_one
- LE.le.antisymm'