mapsTo_insertNth_face_Icc — Mathlib

English

If x ∈ Icc(lower i, upper i), then inserting x at position i maps into the box face Icc.

Русский

Если x лежит в Icc(lower i, upper i), то вставка x на позицию i отображает в Icc-граниbox.

LaTeX

$$$\forall n \; (I : Box (Fin (n + 1))) \; {i : Fin (n + 1)} \; {x : \mathbb{R}},\; x \in Icc (I.lower i) (I.upper i) \Rightarrow \ MapsTo (i.insertNth x) (Icc (I.face i)) Icc I$$$

Lean4

theorem mapsTo_insertNth_face_Icc {n} (I : Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ}
    (hx : x ∈ Icc (I.lower i) (I.upper i)) : MapsTo (i.insertNth x) (Box.Icc (I.face i)) (Box.Icc I) := fun _ hy ↦
  Fin.insertNth_mem_Icc.2 ⟨hx, hy⟩

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