Theorems · Theorem · order theory

IsAntichain.preimage_relEmbedding

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

Defined in

Mathlib.Order.Antichain

Cited by

4 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms