initialSegIic — Mathlib

English

The set Iic(j) = (-∞, j] is an initial segment of α; the projection x ↦ x from Iic(j) into α is an order-embedding.

Русский

Множество Iic(j) = (-∞, j] является начальственным сегментом α; отображение x ↦ x из Iic(j) в α является вложением по порядку.

LaTeX

$$$\text{InitialSeg}(\mathrm{Iic}(j) \to \alpha)$$$

Lean4

/-- `Set.Iic j` is an initial segment. -/
@[simps]
def initialSegIic (j : α) : Set.Iic j ≤i α where
  toFun := fun ⟨j, hj⟩ ↦ j
  inj' _ _ _ := by aesop
  map_rel_iff' := by aesop
  mem_range_of_rel' x k h := by simpa using h.le.trans x.2

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