Relation isomorphisms form a group

instance RelHom.instMonoid {α : Type u_1} {r : α → α → Prop} : Monoid (r →r r)

Equations

• RelHom.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

theorem RelHom.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelHom.id r

theorem RelHom.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r →r r) : f * g = f.comp g

@[simp]

theorem RelHom.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelHom.coe_mul {α : Type u_1} {r : α → α → Prop} (f g : r →r r) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem RelHom.one_apply {α : Type u_1} {r : α → α → Prop} (a : α) : 1 a = a

theorem RelHom.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r →r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

instance RelEmbedding.instMonoid {α : Type u_1} {r : α → α → Prop} : Monoid (r ↪r r)

Equations

• RelEmbedding.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

theorem RelEmbedding.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelEmbedding.refl r

theorem RelEmbedding.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r) : f * g = g.trans f

@[simp]

theorem RelEmbedding.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelEmbedding.coe_mul {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem RelEmbedding.one_apply {α : Type u_1} {r : α → α → Prop} (a : α) : 1 a = a

theorem RelEmbedding.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ↪r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

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

Equations

• RelIso.instGroup = Group.mk ⋯

theorem RelIso.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelIso.refl r

theorem RelIso.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r ≃r r) : f * g = g.trans f

@[simp]

theorem RelIso.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelIso.coe_mul {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

theorem RelIso.one_apply {α : Type u_1} {r : α → α → Prop} (x : α) : 1 x = x

theorem RelIso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

@[simp]

theorem RelIso.inv_apply_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) : e⁻¹ (e x) = x

@[simp]

theorem RelIso.apply_inv_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) : e (e⁻¹ x) = x