English
Let α be a preorder and s be an OrdConnected subset of α. For any x, y in s, the image of the interval Ioc x y under the inclusion map into α equals the interval Ioc of the underlying endpoints, i.e. Subtype.val '' Ioc x y = Ioc x.1 y.
Русский
Пусть α — предпорядок и s ⊆ α удовлетворяет условию OrdConnected. Для любых x, y ∈ s образ множества Ioc x y под включением s в α равен множеству Ioc (x.1) (y.1): Subtype.val '' Ioc x y = Ioc x.1 y.
LaTeX
$$$\forall {\alpha} {s : Set\alpha} [OrdConnected s] (x\,y : s),\; \operatorname{Subtype.val} '' \mathrm{Ioc} x y = \mathrm{Ioc} (x.1) (y.1)$$$
Lean4
@[simp]
theorem image_subtype_val_Ioc {s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Ioc x y = Ioc x.1 y :=
(OrderEmbedding.subtype (· ∈ s)).image_Ioc (by simpa) x y
