English
If f is a strict order opposite (strict anti) map, then DenselyOrdered X ↔ DenselyOrdered Y.
Русский
Если f является строгим антиизоморфизмом порядка, то X и Y имеют плотность порядка эквивалентно друг другу.
LaTeX
$$$ DenselyOrdered(X) \iff DenselyOrdered(Y) $$$
Lean4
theorem denselyOrdered_iff_of_strictAnti {X Y F : Type*} [LinearOrder X] [Preorder Y] [EquivLike F X Y] (f : F)
(hf : StrictAnti f) : DenselyOrdered X ↔ DenselyOrdered Y :=
by
rw [← denselyOrdered_orderDual]
let e : Xᵒᵈ ≃o Y := ⟨OrderDual.ofDual.trans (f : X ≃ Y), ?_⟩
· exact denselyOrdered_iff_of_orderIsoClass e
· simp only [Equiv.trans_apply, EquivLike.coe_coe, OrderDual.forall, OrderDual.ofDual_toDual,
OrderDual.toDual_le_toDual]
intro a b
rw [hf.le_iff_ge]
