image_subtype_val_Ioi_Ioi — Mathlib

English

Let α be a preorder and b ∈ Ioi a. Then Subtype.val '' Ioi b equals Ioi b.1 after projection.

Русский

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

LaTeX

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

Lean4

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

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