Structures · Order
IsPreorder
IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive
and transitive.
- Defined in
- Mathlib.Order.Defs.Unbundled
- Shape
- 2 explicit arguments
Extends2
Extended by2
Concrete types that are instances3
- SimpleGraph
- PFun
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- Antisymmetrization
- toAntisymmetrization
- Set.PartiallyWellOrderedOn.exists_monotone_subseq
- AntisymmRel.setoid
- ofAntisymmetrization
- WellQuasiOrdered.exists_monotone_subseq
- Set.PartiallyWellOrderedOn.wellFoundedOn
- WellQuasiOrdered.wellFounded
- Set.partiallyWellOrderedOn_iff_exists_monotone_subseq
- Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂
- wellQuasiOrdered_iff_exists_monotone_subseq
- Antisymmetrization.ind
- Set.PartiallyWellOrderedOn.pi
- Relation.equivalence_join
- Set.PartiallyWellOrderedOn.prod
- RelEmbedding.isPreorder
- toAntisymmetrization_ofAntisymmetrization
- instInhabitedAntisymmetrization
- Antisymmetrization.induction_on
- instSubsingletonAntisymmetrization
- WellQuasiOrdered.pi
- IsPreorder.toRefl
- IsPreorder.toIsTrans
- IsPreorder.swap
- AntisymmRel.setoid_r
- Order.Preimage.instIsPreorder
- Subrel.instIsPreorderSubtype
- WellQuasiOrdered.prod
- Function.instIsPreorderOnFun
- Function.instIsPreorderSwapProp