Theorems · Theorem · order theory

Set.chainHeight_eq_of_relEmbedding

∀ {α : 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

2 results in Mathlib

Foundations

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