small_proj_preimage_of_locallySmall

English

An instance asserting smallness of the preimage of a locally small set under the projection in CostructuredArrow.

Русский

Пример, доказывающий малость предобраза локально малого множества под проекцией в CostructuredArrow.

LaTeX

$$Small (Set.preimage (StructuredArrow.proj S T).obj 𝒢).Elem$$

Lean4

instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=
  by
  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S.obj G ⟶ T => mk f.2
    by
    rw [this]
    infer_instance
  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩

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