Theorems · Theorem · order theory

denselyOrdered_iff_of_strictAnti

∀ {X : Type u_6} {Y : Type u_7} {F : Type u_8} [inst : LinearOrder X] [inst_1 : Preorder Y] [inst_2 : EquivLike F X Y]
  (f : F), StrictAnti ⇑f → (DenselyOrdered X ↔ DenselyOrdered Y)

Defined in

Mathlib.Order.Hom.Basic

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderPreorderEquivLike