principalSegIio — Mathlib

English

The set Iio(j) = (-∞, j) is a principal segment of α; the projection x ↦ x from Iio(j) into α is a principalSeg.

Русский

Множество Iio(j) = (-∞, j) является принципиальным сегментом α; проекция x ↦ x из Iio(j) в α — принципиальный сегмент.

LaTeX

$$$\text{PrincipalSeg}(\mathrm{Iio}(j) \to \alpha)$$$

Lean4

/-- `Set.Iio j` is a principal segment. -/
@[simps]
def principalSegIio (j : α) : Set.Iio j <i α where
  top := j
  toFun := fun ⟨j, hj⟩ ↦ j
  inj' _ _ _ := by aesop
  map_rel_iff' := by aesop
  mem_range_iff_rel' := by aesop

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