horn_ι_mem_J — Mathlib

English

For each natural number n and index i, the horn inclusion ι in the universal diagram is an element of the class J of morphisms (i.e., the horn inclusion is recognized as part of J).

Русский

Для каждого n и индекса i включение рога ι является элементом класса J морфизмов (включение рога входит в J).

LaTeX

$$$ \\mathrm{horn}_{n+1}^{i} .\\iota \\in J$$$

Lean4

theorem horn_ι_mem_J (n : ℕ) (i : Fin (n + 2)) : J (horn.{u} (n + 1) i).ι :=
  by
  simp only [J, iSup_iff]
  exact ⟨n, ⟨i⟩⟩

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