instSmallFunctorObjIndex — Mathlib

English

The ι component of attachCellsιFunctorObj f πX is Small, i.e., it is a small object in the ambient universe.

Русский

Компонента ι у attachCellsιFunctorObj f πX является маленьким объектом, то есть малый в данной области.

LaTeX

$$$ \text{Small} (\text{attachCellsιFunctorObj } f πX).ι $$$

Lean4

instance : Small.{t} (FunctorObjIndex f πX) :=
  by
  let φ (x : FunctorObjIndex f πX) :
    Σ (i : Shrink.{t} I), Shrink.{t} ((A ((equivShrink _).symm i) ⟶ X) × (B ((equivShrink _).symm i) ⟶ S)) :=
    ⟨equivShrink _ x.i, equivShrink _ ⟨eqToHom (by simp) ≫ x.t, eqToHom (by simp) ≫ x.b⟩⟩
  have hφ : Function.Injective φ := by
    rintro ⟨i₁, t₁, b₁, _⟩ ⟨i₂, t₂, b₂, _⟩ h
    obtain rfl : i₁ = i₂ := by simpa [φ] using congr_arg Sigma.fst h
    simpa [cancel_epi, φ] using h
  exact small_of_injective hφ

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