Relation isomorphisms form a group #
@[simp]
theorem
RelIso.coe_one
{α : Type u_1}
{r : α → α → Prop}
:
↑(RelIso.toRelEmbedding 1).toEmbedding = id
@[simp]
theorem
RelIso.coe_mul
{α : Type u_1}
{r : α → α → Prop}
(e₁ : r ≃r r)
(e₂ : r ≃r r)
:
↑(RelIso.toRelEmbedding (e₁ * e₂)).toEmbedding = ↑(RelIso.toRelEmbedding e₁).toEmbedding ∘ ↑(RelIso.toRelEmbedding e₂).toEmbedding
theorem
RelIso.mul_apply
{α : Type u_1}
{r : α → α → Prop}
(e₁ : r ≃r r)
(e₂ : r ≃r r)
(x : α)
:
↑(RelIso.toRelEmbedding (e₁ * e₂)).toEmbedding x = ↑(RelIso.toRelEmbedding e₁).toEmbedding (↑(RelIso.toRelEmbedding e₂).toEmbedding x)
@[simp]
theorem
RelIso.inv_apply_self
{α : Type u_1}
{r : α → α → Prop}
(e : r ≃r r)
(x : α)
:
↑(RelIso.toRelEmbedding e⁻¹).toEmbedding (↑(RelIso.toRelEmbedding e).toEmbedding x) = x
@[simp]
theorem
RelIso.apply_inv_self
{α : Type u_1}
{r : α → α → Prop}
(e : r ≃r r)
(x : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding (↑(RelIso.toRelEmbedding e⁻¹).toEmbedding x) = x