map — Mathlib

English

If A → B is an isomorphism of presheaves and A is an Ind-object, then B is also an Ind-object.

Русский

Если отображение A → B является изоморфизмом прешепафет, и A является Ind-объектом, то B тоже является Ind-объектом.

LaTeX

$$$\forall A,B\;\forall \eta\colon A\to B\;[\mathrm{IsIso}\;\eta],\; \mathrm{IsIndObject}(A)\to \mathrm{IsIndObject}(B)$$$

Lean4

theorem map {A B : Cᵒᵖ ⥤ Type v} (η : A ⟶ B) [IsIso η] : IsIndObject A → IsIndObject B
  | ⟨⟨P⟩⟩ => ⟨⟨P.extend η⟩⟩

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