Documentation

Mathlib.Order.RelIso.Group

Relation isomorphisms form a group #

instance RelIso.instGroup {α : Type u_1} {r : ααProp} :
Group (r ≃r r)
Equations
@[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