Relation isomorphisms form a group

ink

instance RelIso.instGroupRelIso {α : Type u_1} {r : α → α → Prop} : Group (r ≃r r)

Equations

• RelIso.instGroupRelIso = Group.mk (_ : ∀ (f : r ≃r r), f⁻¹ * f = 1)

ink

@[simp]

theorem RelIso.coe_one {α : Type u_1} {r : α → α → Prop} : ↑(RelIso.toRelEmbedding 1).toEmbedding = id

ink

@[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

ink

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)

ink

@[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

ink

@[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