ind_ind — Mathlib

English

Ind composed with itself equals itself: ind(ind P) = ind P when P implies finitely presentable.

Русский

Пусть P подвигнут к finitely presentable; тогда ind(ind P) = ind P.

LaTeX

$$$ \operatorname{ind}(\operatorname{ind}(P)) = \operatorname{ind}(P) \quad \text{under suitable hypotheses}$$$

Lean4

/-- `ind` is idempotent if `P` implies finitely presentable. -/
theorem ind_ind (hp : P ≤ isFinitelyPresentable.{w} C) [LocallySmall.{w} C] : ind.{w} (ind.{w} P) = ind.{w} P :=
  by
  refine le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind
  have : P.underObj ≤ ObjectProperty.isFinitelyPresentable.{w} (Under X) := fun f hf ↦ hp _ hf
  simpa [ind_iff_ind_underMk, underObj_ind_eq_ind_underObj, ObjectProperty.ind_ind.{w} this] using hf

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