English
If t is an OrdConnected subset of a linear order α with order topology, then the order topology on t coincides with the subspace order topology inherited from α.
Русский
Если t является OrdConnected-подмножеством линейного порядка α с порядковой топологией, то ордерная топология на t совпадает с подпространственной ордерной топологией, индуцированной из α.
LaTeX
$$$\\text{OrderTopology}(t) = \\text{Subtype(Order)}(t)$.$$
Lean4
/-- On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the
order is the same as the restriction to the subset of the order topology. -/
instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α}
[ht : OrdConnected t] : OrderTopology t :=
⟨(Subtype.strictMono_coe t).induced_topology_eq_preorder <| by rwa [← @Subtype.range_val _ t] at ht⟩
