map_map

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.map_map

English

If f ∈ R, then F.map f ∈ R.map F, i.e., map is monotone with respect to inclusion into presieves.

Русский

Если f ∈ R, то F.map f ∈ R.map F, то есть отображение сохраняет включения предсистем.

LaTeX

$$$R f \\Rightarrow (F.map f) \\in R.map F$$$

Lean4

@[grind ←]
theorem map_map {X Y : C} {f : Y ⟶ X} {R : Presieve X} (hf : R f) : R.map F (F.map f) :=
  ⟨hf⟩

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

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

Разделы

Аффилиация

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