Structures · Lean core
Std.Trichotomous
Trichotomous r says that r is trichotomous, that is, ¬ r a b → ¬ r b a → a = b.
- Defined in
- Init.Core
- Shape
- One type argument · adds trichotomous
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Provided automatically by
Concrete types that are instances10
- Nat
- Char
- Subtype
- Prod
- OrderDual
- WithTop
- WithBot
- Sum
- List
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by56
- trichotomous_of
- RelEmbedding.ofMonotone
- trichotomous
- isChain_of_trichotomous
- RelIso.sumLexComplLeft
- DFinsupp.Lex.wellFounded'
- Function.Injective.trichotomous_onFun
- RelIso.sumLexComplRight
- RelEmbedding.trichotomous
- extensional_of_trichotomous_of_irrefl
- IsAntichain.subsingleton
- InvImage.trichotomous
- Std.Trichotomous.swap
- PrincipalSeg.toRelEmbedding_injective
- Pi.trichotomous_lex
- injective_of_increasing
- Finsupp.Lex.wellFounded'
- Concept.codisjoint_extent_intent
- WellFounded.min_eq_of_forall_not_lt
- PrincipalSeg.toRelEmbedding_inj
- Sum.instTrichotomousLex_mathlib
- Sigma.instTotalLexOfTrichotomous
- RelIso.sumLexComplRight_symm_apply
- InitialSeg.subsingleton_of_trichotomous_of_irrefl
- Subrel.instTrichotomousSubtype
- RelIso.sumLexComplLeft_apply
- RelEmbedding.isTrichotomous
- Finsupp.Colex.wellFoundedLT
- IsTrichotomous.swap
- List.Shortlex.trichotomous
- WithBot.trichotomous.lt
- DFinsupp.Colex.wellFoundedLT
- WithTop.trichotomous.lt
- Finsupp.Lex.wellFoundedLT
- trans_trichotomous_left
- RelIso.sumLexComplLeft_symm_apply
- RelHom.injective_of_increasing
- List.Lex.trichotomous
- DFinsupp.Lex.wellFoundedLT
- trans_trichotomous_right
- Pi.isTrichotomous_lex
- WithBot.trichotomous.gt
- WithTop.trichotomous.gt
- Prod.trichotomous
- Std.Trichotomous.decide
- WellFounded.min_image
- RelIso.sumLexComplRight_apply
- RelEmbedding.ofMonotone_coe
- Sigma.instTrichotomousLex
- Function.instTrichotomousSwapProp
Ancestors0
No ancestors.