pullback_eq_top_of_mem

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.pullback_eq_top_of_mem

English

If S f holds for some arrow f, then the pullback of S along f is the top sieve.

Русский

Если S f истинно, то обратное по f от S равно верхнему ситу.

LaTeX

$$$ S f \\rightarrow S.pullback f = \\top $$$

Lean4

theorem pullback_eq_top_of_mem (S : Sieve X) {f : Y ⟶ X} : S f → S.pullback f = ⊤ :=
  (mem_iff_pullback_eq_top f).1

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

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

Разделы

Аффилиация

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