prop_map_succ — Mathlib

English

For i in J, the map homOfLE (Order.le_succ i) composed with iter.F.map has the property Φ.prop.

Русский

Для i в J композиция homOfLE (Order.le_succ i) с map F обладает свойством Φ.prop.

LaTeX

$$$ \\Phi.prop (iter.F.map (\\mathrm{homOfLE} (\\operatorname{Order.le\_succ} i))) $$$

Lean4

theorem prop_map_succ (i : J) (hi : i < j) :
    Φ.prop (iter.F.map (homOfLE (Order.le_succ i) : ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩)) := by
  rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]

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