pretopology_monotone

Mathlib.CategoryTheory.Sites.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.pretopology_monotone

English

If P ≤ Q, then the pretopology generated by P is contained in the pretopology generated by Q, i.e., P.pretopology ≤ Q.pretopology.

Русский

Если P ⊆ Q, то претопология, порождаемая P, содержится в претопологии, порождаемой Q.

LaTeX

$$P.pretopology ≤ Q.pretopology$$

Lean4

theorem pretopology_monotone (hPQ : P ≤ Q) : P.pretopology ≤ Q.pretopology :=
  precoverage_monotone hPQ

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

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

Разделы

Аффилиация

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