Icc — Mathlib

English

There exists an order-embedding from Box ι to sets given by Icc(I.lower, I.upper).

Русский

Существует отображение встраивания сохранения порядка из Box ι в множества, задаваемые Icc(I.lower, I.upper).

LaTeX

$$$ Box.Icc : Box ι \\hookrightarrow_o Set (ι \\to ℝ) $ defined by I \\mapsto \\{ x : ι \\to ℝ \\mid I.lower \\le x \\le I.upper \\}$$$

Lean4

/-- Closed box corresponding to `I : BoxIntegral.Box ι`. -/
protected def Icc : Box ι ↪o Set (ι → ℝ) :=
  OrderEmbedding.ofMapLEIff (fun I : Box ι ↦ Icc I.lower I.upper) fun I J ↦ (le_TFAE I J).out 2 0

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