Theorems · Theorem · order theory

RelIso.trans_apply

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

Defined in

Mathlib.Order.RelIso.Basic

Cited by

4 results in Mathlib

Foundations

Depth 24 from the axioms · uses Quot.sound