castSucc_mem_finset_iff — Mathlib

English

Gives an equivalence: map' f x equals y.castSucc iff x ≤ (f y).castSucc and for all i < y we have (f i).castSucc < x.

Русский

Даёт эквивалентность: map' f x = y.castSucc тогда и только тогда, когда x ≤ (f y).castSucc и для всех i < y выполняется (f i).castSucc < x.

LaTeX

$$$map' f x = y.castSucc \iff x \le (f y).castSucc \land \forall i < y, (f i).castSucc < x.$$$

Lean4

@[simp]
theorem castSucc_mem_finset_iff (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (i : Fin (n + 1)) :
    i.castSucc ∈ finset f x ↔ x ≤ (f i).castSucc := by simp [mem_finset_iff, Fin.castPred_castSucc]

Похожие утверждения