English
DenselyOrdered X is equivalent to DenselyOrdered Y if X and Y are connected by an order-isomorphism class F.
Русский
Плотность порядка X эквивалентна плотности порядка Y, если X и Y связаны классом порядковых изоморфизмов F.
LaTeX
$$$ DenselyOrdered(X) \iff DenselyOrdered(Y) $$$
Lean4
theorem denselyOrdered_iff_of_orderIsoClass {X Y F : Type*} [Preorder X] [Preorder Y] [EquivLike F X Y]
[OrderIsoClass F X Y] (f : F) : DenselyOrdered X ↔ DenselyOrdered Y :=
by
constructor
· intro H
refine ⟨fun a b h ↦ ?_⟩
obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)
exact ⟨f c, by simpa using hc⟩
· intro H
refine ⟨fun a b h ↦ ?_⟩
obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
exact ⟨EquivLike.inv f c, by simpa using hc⟩
