Relation isomorphisms form a group

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

Equations

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

@[simp]

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

@[simp]

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

theorem RelIso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ : r ≃r r) (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