ofOpSequence_map_homOfLE_succ — Mathlib

English

The op-version of the map lemma: the map with op at homOfLE corresponds to f n.

Русский

Лемма для противоположного варианта отображения: отображение с оп-представлением через homOfLE даёт f n.

LaTeX

$$@[simp] theorem ofOpSequence_map_homOfLE_succ (n : ℕ) : (ofOpSequence f).map (homOfLE (Nat.le_add_right n 1)).op = f n$$

Lean4

@[simp]
theorem ofOpSequence_map_homOfLE_succ (n : ℕ) : (ofOpSequence f).map (homOfLE (Nat.le_add_right n 1)).op = f n := by
  simp [ofOpSequence]

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