mathlib3 documentation

order.rel_iso.group

Relation isomorphisms form a group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def rel_iso.group {α : Type u_1} {r : α → α → Prop} :
group (r ≃r r)
Equations
source
@[simp]
theorem rel_iso.coe_one {α : Type u_1} {r : α → α → Prop} :
⇑1 = id
source
@[simp]
theorem rel_iso.coe_mul {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) :
⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
source
theorem rel_iso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α) :
⇑(e₁ * e₂) x = ⇑e₁ (⇑e₂ x)
source
@[simp]
theorem rel_iso.inv_apply_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
⇑e⁻¹ (⇑e x) = x
source
@[simp]
theorem rel_iso.apply_inv_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
⇑e (⇑e⁻¹ x) = x