principalSegIioIicOfLE — Mathlib

English

If i ≤ j, then the open interval Iio(i) is a principal segment of Iic(j): it is the initial part of Iic(j) determined by i.

Русский

Если i ≤ j, то открытый интервал Iio(i) является главным сегментом Iic(j): это начальная часть Iic(j), ограниченная i.

LaTeX

$$$\\{ i \\le j \\} \\Rightarrow \\mathrm{Iio}(i) \\

Lean4

/-- If `i ≤ j`, then `Set.Iio i` is a principal segment of `Set.Iic j`. -/ @[simps top] def principalSegIioIicOfLE {i j : α} (h : i ≤ j) : Set.Iio i <i Set.Iic j where top := ⟨i, h⟩ toFun := fun ⟨k, hk⟩ ↦ ⟨k, hk.le.trans h⟩ inj' _ _ _ := by aesop map_rel_iff' := by aesop mem_range_iff_rel' := by aesop

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