mapsTo_insertNth_face — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mapsTo_insertNth_face {n} (I : Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ}
    (hx : x ∈ Ioc (I.lower i) (I.upper i)) : MapsTo (i.insertNth x) (I.face i : Set (_ → _)) (I : Set (_ → _)) :=
  by
  intro y hy
  simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same, Fin.insertNth_apply_succAbove]
  exact ⟨hx, hy⟩

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