English
A simplified version of the previous criterion, with minor notational adjustments, establishing the same equivalence.
Русский
Упрощённая версия предыдущей эквивалентности с небольшими обозначениями, сохраняющая эквивалентность.
LaTeX
$$$(\text{same as above with minor notational changes})$$$
Lean4
theorem map'_eq_castSucc_iff (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (y : Fin (n + 1)) :
map' f x = y.castSucc ↔ x ≤ (f y).castSucc ∧ ∀ (i : Fin (n + 1)) (_ : i < y), (f i).castSucc < x :=
by
simp only [map', Finset.min'_eq_iff, castSucc_mem_finset_iff, and_congr_right_iff]
intro h
constructor
· intro h' i hi
by_contra!
exact hi.not_ge (by simpa using h' i.castSucc (by simpa))
· intro h' i hi
obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
· simp only [Fin.castSucc_le_castSucc_iff]
by_contra!
exact (h' i this).not_ge (by simpa using hi)
· apply Fin.le_last
