image_subtype_val_Ioi_Ici — Mathlib

English

Let α be a preorder and let b be a point in the interval Ioi a. Then the image of Ici(b) under the natural projection Subtype.val is exactly the interval Ici(b.1) in α.

Русский

Пусть α упорядочено; для любого b ∈ Ioi(a) образ множества Ici(b) под отображением Subtype.val равен интервалу Ici(b₁) на α.

LaTeX

$$$\mathrm{image}(\mathrm{Subtype.val}, \mathrm{Ici}(b)) = \mathrm{Ici}(b_1)$$$

Lean4

@[simp]
theorem image_subtype_val_Ioi_Ici {a : α} (b : Ioi a) : Subtype.val '' Ici b = Ici b.1 :=
  (Subtype.image_preimage_val (Ioi a) (Ici b.1)).trans <| inter_eq_right.2 <| Ici_subset_Ioi.2 b.2

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