Relation homomorphisms, embeddings, isomorphisms #
This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and isomorphisms.
Main declarations #
RelHom
: Relation homomorphism. ARelHom r s
is a functionf : α → β
such thatr a b → s (f a) (f b)
.RelEmbedding
: Relation embedding. ARelEmbedding r s
is an embeddingf : α ↪ β
such thatr a b ↔ s (f a) (f b)
.RelIso
: Relation isomorphism. ARelIso r s
is an equivalencef : α ≃ β
such thatr a b ↔ s (f a) (f b)
.sumLexCongr
,prodLexCongr
: Creates a relation homomorphism between twoSum.Lex
or twoProd.Lex
from relation homomorphisms between their arguments.
Notation #
→r
:RelHom
↪r
:RelEmbedding
≃r
:RelIso
A relation homomorphism with respect to a given pair of relations r
and s
is a function f : α → β
such that r a b → s (f a) (f b)
.
Equations
Instances For
RelHomClass F r s
asserts that F
is a type of functions such that all f : F
satisfy r a b → s (f a) (f b)
.
The relations r
and s
are outParam
s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
- map_rel (f : F) {a b : α} : r a b → s (f a) (f b)
A
RelHomClass
sends related elements to related elements
Instances
The map coe_fn : (r →r s) → (α → β)
is injective.
An increasing function is injective
An increasing function is injective
A relation embedding with respect to a given pair of relations r
and s
is an embedding f : α ↪ β
such that r a b ↔ s (f a) (f b)
.
- toFun : α → β
Elements are related iff they are related after apply a
RelEmbedding
Instances For
A relation embedding with respect to a given pair of relations r
and s
is an embedding f : α ↪ β
such that r a b ↔ s (f a) (f b)
.
Equations
Instances For
The map coe_fn : (r ↪r s) → (α → β)
is injective.
Identity map is a relation embedding.
Equations
Instances For
Quotient.mk
as a relation homomorphism between the relation and the lift of a relation.
Equations
Instances For
Quotient.out
as a relation embedding between the lift of a relation and the relation.
Equations
Instances For
Alias of the reverse direction of wellFounded_lift₂_iff
.
A relation is well founded iff its lift to a quotient is.
Alias of the forward direction of wellFounded_lift₂_iff
.
A relation is well founded iff its lift to a quotient is.
Alias of the forward direction of wellFounded_liftOn₂'_iff
.
Alias of the reverse direction of wellFounded_liftOn₂'_iff
.
To define a relation embedding from an antisymmetric relation r
to a reflexive relation s
it suffices to give a function together with a proof that it satisfies s (f a) (f b) ↔ r a b
.
Equations
Instances For
It suffices to prove f
is monotone between strict relations
to show it is a relation embedding.
Equations
Instances For
Sum.inl
as a relation embedding into Sum.LiftRel r s
.
Equations
Instances For
Sum.inr
as a relation embedding into Sum.LiftRel r s
.
Equations
Instances For
A relation isomorphism is an equivalence that is also a relation embedding.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
Elements are related iff they are related after apply a
RelIso
Instances For
A relation isomorphism is an equivalence that is also a relation embedding.
Equations
Instances For
Convert a RelIso
to a RelEmbedding
. This function is also available as a coercion
but often it is easier to write f.toRelEmbedding
than to write explicitly r
and s
in the target type.
Equations
Instances For
The map DFunLike.coe : (r ≃r s) → (α → β)
is injective.
See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because RelIso
defines custom coercions other than the ones given by DFunLike
.
Equations
Instances For
Identity map is a relation isomorphism.
Equations
Instances For
A surjective relation embedding is a relation isomorphism.
Equations
Instances For
Transport a RelHom
across a pair of RelIso
s, by pre- and post-composition.
This is Equiv.arrowCongr
for RelHom
.
Equations
Instances For
Given relation isomorphisms r₁ ≃r s₁
and r₂ ≃r s₂
, construct a relation isomorphism for the
lexicographic orders on the sum.
Equations
Instances For
Given relation isomorphisms r₁ ≃r s₁
and r₂ ≃r s₂
, construct a relation isomorphism for the
lexicographic orders on the product.
Equations
Instances For
Alias of RelIso.ofUniqueOfIrrefl
.
Two irreflexive relations on a unique type are isomorphic.
Equations
Instances For
Alias of RelIso.ofUniqueOfRefl
.
Two reflexive relations on a unique type are isomorphic.