Structures · Lean core
Std.Asymm
Asymm r means that the binary relation r is asymmetric, that is, r a b → ¬ r b a.
- Defined in
- Init.Core
- Shape
- One type argument · adds asymm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Concrete types that are instances6
- Char
- Vector
- Subtype
- Prod
- List
- Array
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- asymm
- RelEmbedding.ofMonotone
- Std.Asymm.irrefl
- asymm_of
- Std.Asymm.antisymm
- Std.Asymm.swap
- RelEmbedding.asymm
- RelHomClass.asymm
- Function.instAsymmOnFun
- Std.Asymm.isIrrefl
- List.Lex.asymm
- InvImage.asymm
- IsAsymm.isAntisymm
- IsAsymm.isIrrefl
- Sigma.instAntisymmLexOfAsymm
- Order.Preimage.instAsymm
- Prod.instAsymmLex_mathlib
- List.Shortlex.asymm
- RelEmbedding.ofMonotone_coe
- RelEmbedding.isAsymm
- Function.instAsymmSwapProp
- Subrel.instAsymmSubtype
- Std.Asymm.isAntisymm
- isStrictWeakOrder_of_isOrderConnected
- Std.Asymm.decide
- RelEmbedding.ofMonotone.congr_simp
- RelHomClass.isAsymm
- IsAsymm.swap