principalSegIioIicOfLE_toRelEmbedding

English

Let i ≤ j and k ∈ Iio(i). The embedding from principalSegIioIicOfLE(h) to the ambient order sends k to the pair ⟨k.1, k.2.le.trans h⟩, i.e. it uses the underlying value with the appropriate bound.

Русский

Пусть i ≤ j и k ∈ Iio(i). Вложение из principalSegIioIicOfLE(h) в надмножество отправляет k в пару ⟨k.1, k.2.le.trans h⟩, то есть использует основанное значение с соответствующим ограничением.

LaTeX

$$$(\\mathrm{principalSegIioIicOfLE}(h)).\\mathrm{toRelEmbedding}(k) = \\langle k.1, k.2.\\text{le}.trans(h) \\rangle$$$

Lean4

@[simp]
theorem principalSegIioIicOfLE_toRelEmbedding {i j : α} (h : i ≤ j) (k : Iio i) :
    (Set.principalSegIioIicOfLE h).toRelEmbedding k = ⟨k, k.2.le.trans h⟩ :=
  rfl

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