English
Definition of succAboveOrderIso: an explicit order isomorphism from Fin(n+1) to the complement of a singleton {i} in Fin(n+2) given by i.succAboveOrderEmb.
Русский
Определение succAboveOrderIso: явный порядок-изоморфизм Fin(n+1) к {i}ᶜ в Fin(n+2) через i.succAboveOrderEmb.
LaTeX
$$$\text{succAboveOrderIso} : \mathrm{Fin}(n+1) \cong_o \{i\}^{c} \subseteq \mathrm{Fin}(n+2).$$$
Lean4
theorem pi_lex_lt_cons_cons {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} (s : ∀ {i : Fin n.succ}, α i → α i → Prop) :
Pi.Lex (· < ·) (@s) (Fin.cons x₀ x) (Fin.cons y₀ y) ↔
s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (· < ·) (@fun i : Fin n ↦ @s i.succ) x y :=
by
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_iff_succ]
simp [and_assoc, exists_and_left]
