Theorems · Theorem · order theory

IsChain.image

∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} [inst : FunLike F α β]
  [RelHomClass F r r'], IsChain r s → ∀ (φ : F), IsChain r' (⇑φ '' s)

Defined in

Mathlib.Order.Preorder.Chain

Cited by

8 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

FunLikeRelHomClass