Documentation

Mathlib.Order.RelIso.Group

Relation isomorphisms form a group #

instance RelIso.instGroup {α : Type u_1} {r : ααProp} :
Equations
@[simp]
theorem RelIso.coe_one {α : Type u_1} {r : ααProp} :
@[simp]
theorem RelIso.coe_mul {α : Type u_1} {r : ααProp} (e₁ e₂ : r ≃r r) :
(e₁ * e₂) = e₁ e₂
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 : α) :