sequentialFunctor_final — Mathlib

English

The sequentialFunctor J is Final.

Русский

Последовательный функтор J является конечным (Final).

LaTeX

$$$ (\\text{sequentialFunctor } J).\\text{Final} $$$

Lean4

instance sequentialFunctor_final : (sequentialFunctor J).Final where
  out
    d := by
    obtain ⟨n, (g : d ≤ (sequentialFunctor J).obj n)⟩ := sequentialFunctor_final_aux J d
    have : Nonempty (StructuredArrow d (sequentialFunctor J)) := ⟨StructuredArrow.mk (homOfLE g)⟩
    apply isConnected_of_zigzag
    refine fun i j ↦ ⟨[j], ?_⟩
    simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq, not_false_eq_true,
      List.getLast_cons, List.getLast_singleton', reduceCtorEq]
    clear! C
    wlog h : j.right ≤ i.right
    · exact or_comm.1 (this J d n g inferInstance j i (le_of_lt (not_le.mp h)))
    · right
      exact ⟨StructuredArrow.homMk (homOfLE h) rfl⟩

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