predAboveOrderHom — Mathlib

English

For a fixed p ∈ Fin n, the map a ↦ p.predAbove a is an order-homomorphism from Fin (n+1) to Fin n.

Русский

Для фиксированного p ∈ Fin n отображение a ↦ p.predAbove a является гомоморфизмом порядка от Fin(n+1) к Fin n.

LaTeX

$$$\forall {p : \mathrm{Fin}(n)}, \; (\lambda a : \mathrm{Fin}(n+1) \mapsto p.predAbove a) : \mathrm{Fin}(n+1) \too \mathrm{Fin}(n)$ является однообразным отображением по порядку$$

Lean4

/-- `Fin.predAbove p` as an `OrderHom`. -/
@[simps!]
def predAboveOrderHom (p : Fin n) : Fin (n + 1) →o Fin n :=
  ⟨p.predAbove, p.predAbove_right_monotone⟩

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