sectionsMk_val_op_bot — Mathlib

English

Compatibility of sectionsMK with maps between different i and j is ensured, i.e., the lifting respects functorial maps.

Русский

Совместимость секций с отображениями между разными i и j обеспечивается: тяготение сохраняет функторность.

LaTeX

$$$\\text{compatibility}$$$

Lean4

theorem sectionsMk_val_op_bot (val₀ : F.obj (op ⊥)) : (d.sectionsMk val₀).val (op ⊥) = val₀ := by
  simpa using (default : d.Extension val₀ ⊥).map_zero

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