English
The order isomorphism preserves the order relation in the natural way: a ≤ b in Fin(n+1) iff their images satisfy the corresponding order in the complement Finset.
Русский
При этом изоморфизме порядок сохраняется: a ≤ b в Fin(n+1) эквивалентно тому, что их изображения удовлетворяют соответствующему порядку в дополнении.
LaTeX
$$Iff (RelIso.instFunLike.coe (SuccAboveOrderIso i) a ≤ ... ) (inst.le a b).$$
Lean4
theorem insertNth_mem_Icc {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q₁ q₂ : ∀ j, α j} :
i.insertNth x p ∈ Icc q₁ q₂ ↔
x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j) :=
by simp only [mem_Icc, insertNth_le_iff, le_insertNth_iff, and_assoc, @and_left_comm (x ≤ q₂ i)]
