subtype_functor_final — Mathlib

English

For any linear order J and any j ∈ J, the inclusion of the upper tail {x ∈ J | j ≤ x} into J is a final functor.

Русский

Для любого линейно упорядоченного множества J и элемента j ∈ J включение верхней «хвостовой» части {x ∈ J | j ≤ x} в J является финальным функтором.

LaTeX

$$$$ \\text{The inclusion } \\{x \\in J \\mid j \\le x\\} \\hookrightarrow J \\text{ is final.} $$$$

Lean4

instance subtype_functor_final {J : Type u} [LinearOrder J] (j : J) : (Subtype.mono_coe (Set.Ici j)).functor.Final :=
  by
  rw [Monotone.final_functor_iff]
  intro k
  exact ⟨⟨max j k, le_max_left _ _⟩, le_max_right _ _⟩

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