Structures · Order
IsEquiv
IsEquiv X r means that the binary relation r on X is an equivalence relation, that
is, IsPreorder X r and Std.Symm r.
- Defined in
- Mathlib.Order.Defs.Unbundled
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Path
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- Relation.EqvGen.eqvGen_le
- Set.Nonempty.pairwise_iff_exists_forall
- Equivalence.of_isEquiv
- Set.pairwise_iff_exists_forall
- List.IsChain.length_le_length_destutter
- List.length_destutter'_congr
- List.le_length_destutter'_cons
- List.length_destutter_le_length_destutter_cons
- Function.instIsEquivSwapProp
- IsEquiv.comap
- Function.instIsEquivOnFun
- Order.Preimage.instIsEquiv
- IsEquiv.toIsPreorder
- IsEquiv.toSymm