English
For i ∈ Fin(n+1), x ∈ α i, p ∈ ∀ j, α (i.succAbove j), the preimage of the pointwise interval Icc under i.insertNth x is the pointwise interval shifted by i.succAbove.
Русский
Для i ∈ Fin(n+1), x ∈ α i, p ∈ ∀ j, α (i.succAbove j), предобразок точки по точечному интервалу Icc под i.insertNth x равен точечному интервалу, смещённому по i.succAbove.
LaTeX
$$$ (i.insertNth x)^{-1} Icc(q_1,q_2) = Icc(\lambda j. q_1(i.succAbove j)) (\lambda j. q_2(i.succAbove j)). $$$
Lean4
theorem preimage_insertNth_Icc_of_mem {i : Fin (n + 1)} {x : α i} {q₁ q₂ : ∀ j, α j} (hx : x ∈ Icc (q₁ i) (q₂ i)) :
i.insertNth x ⁻¹' Icc q₁ q₂ = Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j) :=
Set.ext fun p ↦ by simp only [mem_preimage, insertNth_mem_Icc, hx, true_and]
