Documentation

Mathlib.Order.RelIso.Group

Relation isomorphisms form a group #

instance RelIso.instGroupRelIso {α : Type u_1} {r : ααProp} :
Group (r ≃r r)
Equations
@[simp]
theorem RelIso.coe_one {α : Type u_1} {r : ααProp} :
(RelIso.toRelEmbedding 1).toEmbedding = id
@[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
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)
@[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
@[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