Theorems · Theorem · order theory

IsAntichain.image_relEmbedding

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsAntichain r s → ∀ (φ : r ↪r r'), IsAntichain r' (⇑φ '' s)

Defined in

Mathlib.Order.Antichain

Cited by

4 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext