English
For a directed relation r with a function f, the natural-number indexed sequence f hf.sequence f is monotone in the sense of r: for every n, r(f(hf.sequence f n), f(hf.sequence f (n+1))).
Русский
Пусть r направлена на β и есть функция f. Последовательность f hf.sequence f по индексам нат является возрастающей по отношению r: для каждого n выполняется r( f(hf.sequence f n), f(hf.sequence f (n+1)) ).
LaTeX
$$$ r\bigl(f( hf.sequence f n )\bigr)\bigl( f( hf.sequence f (n+1) ) \bigr) $$
Lean4
theorem sequence_mono_nat {r : β → β → Prop} {f : α → β} (hf : Directed r f) (n : ℕ) :
r (f (hf.sequence f n)) (f (hf.sequence f (n + 1))) :=
by
dsimp [Directed.sequence]
generalize hf.sequence f n = p
rcases (decode n : Option α) with - | a
· exact (Classical.choose_spec (hf p p)).1
· exact (Classical.choose_spec (hf p a)).1
