Theorems · Theorem · order theory

Set.chainHeight_eq_of_relIso

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} (s : Set α) (e : r ≃r r'),
  (⇑e '' s).chainHeight r' = s.chainHeight r

Defined in

Mathlib.Order.Height

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound