pullback_inter

Mathlib.CategoryTheory.Sites.Sieves

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

English

Pullback distributes over intersection: for any S, R on X, the pullback along f of S ⊓ R equals the intersection of the pullbacks.

Русский

Обратное по f к S ⊓ R равно S.pullback f ⊓ R.pullback f.

LaTeX

$$$ (S \\sqcap R).pullback f = S.pullback f \\sqcap R.pullback f $$$

Lean4

@[simp]
theorem pullback_inter {f : Y ⟶ X} (S R : Sieve X) : (S ⊓ R).pullback f = S.pullback f ⊓ R.pullback f := by
  simp [Sieve.ext_iff]

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

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

Разделы

Аффилиация

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