to_middle_condition

Mathlib.CategoryTheory.Sites.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition

← MathLib Explorer

English

For I in (S.bind T).Arrow, the middle refinement satisfies the middle condition (toMiddle).

Русский

Для I в (S.bind T).Arrow выполняется условие середины (toMiddle).

LaTeX

$$$(T I.fromMiddle) I.toMiddleHom$$$

Lean4

theorem to_middle_condition {X : C} {S : J.Cover X} {T : ∀ I : S.Arrow, J.Cover I.Y} (I : (S.bind T).Arrow) :
    (T I.fromMiddle) I.toMiddleHom :=
  I.hf.choose_spec.choose_spec.choose_spec.choose_spec.1

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

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

Разделы

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

Аффилиация

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