English
For a relation r on a type with transitivity, lifting Functor preserves the succ-step characterization: ((· < ·) ⇒ r) f f is equivalent to a universal condition on the finite predecessors castSucc and succ.
Русский
Для отношения r на тип с транситивностью подъём функции сохраняет характеристику перехода по Succ: эквивалентность между левой и правой частями условия на f.
LaTeX
$$$\\forall {\\alpha} (r : \\alpha \\to \\alpha \\to \\mathrm{Prop}) [IsTrans \\alpha r] {f : \\mathrm{Fin}(n + 1) \\to \\alpha},\\\\n ((\\cdot < \\cdot) \\Rightarrow r) f f \\ \\Longleftrightarrow\\ \\forall i : \\mathrm{Fin}(n), r (f (\\mathrm{castSucc} \\ i)) (f i.succ)$$$
Lean4
theorem liftFun_iff_succ {α : Type*} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} :
((· < ·) ⇒ r) f f ↔ ∀ i : Fin n, r (f (castSucc i)) (f i.succ) :=
by
constructor
· intro H i
exact H i.castSucc_lt_succ
· refine fun H i => Fin.induction (fun h ↦ ?_) ?_
· simp at h
· intro j ihj hij
rw [← le_castSucc_iff] at hij
obtain hij | hij := (le_def.1 hij).eq_or_lt
· obtain rfl := Fin.ext hij
exact H _
· exact _root_.trans (ihj hij) (H j)
