image_subtype_val_Ico — Mathlib

English

For an OrdConnected set s and x,y ∈ s, the image of Ico x y under Subtype.val equals Ico x.1 y.1

Русский

Пусть s OrdConnected. Тогда образ Ico(x,y) под Subtype.val равен Ico(x.1, y.1).

LaTeX

$$$\mathrm{Subtype.val}''\mathrm{Ico}(x,y) = \mathrm{Ico}(x.1, y.1).$$$

Lean4

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

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