Theorems · Theorem · order theory

RelIso.symm_trans_apply

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s)
  (g : s ≃r t) (a : γ), (f.trans g).symm a = f.symm (g.symm a)

Defined in

Mathlib.Order.RelIso.Basic

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound