Structures · Lean core
Std.Irrefl
Irrefl r means the binary relation r is irreflexive, that is, r x x never holds.
- Defined in
- Init.Core
- Shape
- One type argument · adds irrefl
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances8
- Char
- Vector
- Subtype
- Prod
- Sum
- List
- Sigma
- Array
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- irrefl
- irrefl_of
- Pi.lex_iff_of_unique
- List.Subset.antisymm_of_pairwise
- List.Pairwise.nodup
- DFinsupp.lex_iff_of_unique
- List.Pairwise.eq_of_mem_iff
- Finite.wellFounded_of_trans_of_irrefl
- Relation.acc_of_singleton
- RelEmbedding.irrefl
- Relation.cutExpand_iff
- List.shortlex_cons_iff
- extensional_of_trichotomous_of_irrefl
- RelIso.ofUniqueOfIrrefl
- IncompRel.refl
- PrincipalSeg.toRelEmbedding_injective
- Finsupp.lex_iff_of_unique
- not_rel_of_subsingleton
- injective_of_increasing
- RelHomClass.irrefl
- Cycle.Chain.eq_nil_of_irrefl
- List.lex_cons_iff
- Concept.disjoint_extent_intent
- Acc.cutExpand
- ne_of_irrefl
- Relation.not_cutExpand_zero
- PrincipalSeg.toRelEmbedding_inj
- Relation.cutExpand_le_invImage_lex
- SetRel.instIsIrreflOfPredProdMatch_1PropOfIrrefl
- InvImage.irreflexive
- Std.Irrefl.compl
- Prod.instIrreflLex_mathlib
- InitialSeg.subsingleton_of_trichotomous_of_irrefl
- Sum.instIrreflLiftRel_mathlib
- RelHomClass.isIrrefl
- Function.instIrreflSwapProp
- Subrel.instIrreflSubtype
- Sum.instIrreflLex_mathlib
- Std.Irrefl.swap
- eq_empty_relation
- Subsingleton.isWellOrder
- Order.Preimage.instIrrefl
- RelHom.injective_of_increasing
- Function.instIrreflOnFun
- ne_of_irrefl'
- Sigma.instIrreflLex
- Relation.cutExpand_closed
- InvImage.irrefl
- List.Shortlex.cons
- RelEmbedding.isIrrefl
Ancestors0
No ancestors.