restrictionLT_map — Mathlib

English

ObjMap respects identity morphisms: the image of the identity morphism is the identity on the image object.

Русский

ObjMap сохраняет тождественные морфизмы: образ тождества равен тождеству на образе.

LaTeX

$$objMap I κ (𝟙 f) = 𝟙 _$$

Lean4

@[simp]
theorem restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) :
    (restrictionLT F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) :=
  rfl

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