section_comp_left

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.section_comp_left

← MathLib Explorer

English

For a reflexive pair f,g, we have commonSection f g ≫ f = id_B.

Русский

Для рефлексивной пары f,g имеет место commonSection f g ∘ f = id_B.

LaTeX

$$$\operatorname{commonSection}(f,g) \circ f = \mathrm{id}_B$$$

Lean4

@[reassoc (attr := simp)]
theorem section_comp_left (f g : A ⟶ B) [IsReflexivePair f g] : commonSection f g ≫ f = 𝟙 B :=
  (IsReflexivePair.common_section f g).choose_spec.1

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru