rel_sequence — Mathlib

English

For a directed r and f, the relation between f a and f of the next element is established by the next step: r (f a) (f (hf.sequence f (encode a + 1))).

Русский

Для направленной relation и функции f связь между f a и следующим элементом устанавливается на следующем шаге: r(f a, f(hf.sequence f(encode a + 1))).

LaTeX

$$$ r\bigl( f a \bigr)\bigl( f\bigl( hf.sequence f (\mathrm{encode} a + 1) \bigr) \bigr) $$$

Lean4

theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) :
    r (f a) (f (hf.sequence f (encode a + 1))) :=
  by
  simp only [Directed.sequence, encodek]
  exact (Classical.choose_spec (hf _ a)).2

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