English
Characterizes when map' f x equals castSucc of y; it is equivalent to x ≤ (f y).castSucc and a universal condition on i < y.
Русский
Характеризация равенства map' f x = y.castSucc: это эквивалентно x ≤ (f y).castSucc и условию для всех i < y.
LaTeX
$$$map' f x = y.castSucc \iff x \le (f y).castSucc \land \forall i < y, (f i).castSucc < x.$$$
Lean4
theorem map'_eq_last_iff (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) :
map' f x = Fin.last _ ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x :=
by
simp only [map', Finset.min'_eq_iff, last_mem_finset, Fin.last_le_iff, true_and]
constructor
· intro h i
by_contra!
exact i.castSucc_ne_last (h i.castSucc (by simpa))
· intro h i hi
by_contra!
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last this
simp only [castSucc_mem_finset_iff] at hi
exact hi.not_gt (h i)
