image_subtype_val_Ioo — Mathlib

English

Let α be a preorder and s ⊆ α OrdConnected. For any x, y in s, the image of Ioo x y under the inclusion map into α equals the interval Ioo of the endpoints, i.e. Subtype.val '' Ioo x y = Ioo x.1 y.

Русский

Пусть α — предпорядок и s ⊆ α удовлетворяет OrdConnected. Для любых x, y ∈ s образ подмножества Ioo x y через включение в α равен Ioo (x.1) (y.1): Subtype.val '' Ioo x y = Ioo x.1 y.

LaTeX

$$$\forall {\alpha} {s : Set\alpha} [OrdConnected s] (x\,y : s),\; \operatorname{Subtype.val} '' \mathrm{Ioo} x y = \mathrm{Ioo} (x.1) (y.1)$$$

Lean4

@[simp]
theorem image_subtype_val_Ioo {s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Ioo x y = Ioo x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ioo (by simpa) x y

Похожие утверждения