English
If i ≤ j, then the lower closed interval Iic(i) sits inside Iic(j) as an initial segment; there is an order-embedding from Iic(i) to Iic(j) given by mapping ⟨k, hk⟩ to ⟨k, hk.trans h⟩, which preserves order.
Русский
Если i ≤ j, то нижний замкнутый интервал Iic(i) входит в Iic(j) как начальный сегмент; существует упорядочивающее вложение Iic(i) → Iic(j), заданное отображением ⟨k, hk⟩ ↦ ⟨k, hk.trans h⟩, сохраняющее порядок.
LaTeX
$$$\\forall i,j\\, (h: i \\le j),\, \\mathrm{Iic}(i) \\le_i \\mathrm{Iic}(j).$$$
Lean4
/-- If `i ≤ j`, then `Set.Iic i` is an initial segment of `Set.Iic j`. -/
@[simps]
def initialSegIicIicOfLE {i j : α} (h : i ≤ j) : Set.Iic i ≤i Set.Iic j
where
toFun := fun ⟨k, hk⟩ ↦ ⟨k, hk.trans h⟩
inj' _ _ _ := by aesop
map_rel_iff' := by aesop
mem_range_of_rel' x k h := ⟨⟨k.1, (Subtype.coe_le_coe.2 h.le).trans x.2⟩, rfl⟩
