Structures · Lean core
Std.Antisymm
Antisymm r says that r is antisymmetric, that is, r a b → r b a → a = b.
- Defined in
- Init.Core
- Shape
- One type argument · adds antisymm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Concrete types that are instances11
- Nat
- Char
- String.Pos.Raw
- String.Slice.Pos
- String.Pos
- ZFSet
- Subtype
- Prod
- Sum
- List
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by61
- Finset.sort
- Multiset.sort
- antisymm
- List.Perm.eq_of_pairwise'
- Finset.length_sort
- Finset.pairwise_sort
- Finset.sort_nodup
- Multiset.sort.congr_simp
- Multiset.sort_eq
- List.sublist_of_subperm_of_pairwise
- Finset.sort_eq
- List.Subset.antisymm_of_pairwise
- Finset.mem_sort
- Multiset.length_sort
- Multiset.pairwise_sort
- AntisymmRel.eq
- List.Pairwise.eq_of_mem_iff
- Finset.sort_cons
- antisymm_iff
- antisymm_of
- Finset.sort.congr_simp
- RelEmbedding.antisymm
- List.toFinset_sort
- Multiset.sort_zero
- Finset.sort_toFinset
- Finset.sort_val
- Multiset.sort_singleton
- List.sublist_insertionSort'
- antisymm'
- Function.Injective.antisymm_onFun
- List.orderedInsert_erase
- List.mergeSort_eq_insertionSort
- Order.Preimage.antisymm
- antisymmRel_iff_eq
- Multiset.mem_sort
- Multiset.map_sort
- RelEmbedding.ofMapRelIff
- Multiset.sort_cons
- List.mergeSort_eq_self
- Finset.sort_perm_toList
- Finset.sort_empty
- Finset.map_sort
- Finset.sort_mk
- Std.Antisymm.decide
- Sum.instAntisymmLex_mathlib
- RelEmbedding.isAntisymm
- List.Pairwise.destutter_eq_dedup
- Order.Preimage.isAntisymm
- IsAntichain.isAntisymm
- antisymm_of'