precoverage_monotone

Mathlib.CategoryTheory.Sites.MorphismProperty

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

English

If hPQ: P ≤ Q then precoverage P ≤ precoverage Q.

Русский

Если hPQ: P ≤ Q, то предокрытие P ≤ предокрытие Q.

LaTeX

$$Theorem: precoverage_monotone (hPQ) : precoverage P ≤ precoverage Q$$

Lean4

theorem precoverage_monotone (hPQ : P ≤ Q) : precoverage P ≤ precoverage Q := fun _ _ hR _ _ hg ↦ hPQ _ (hR hg)

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

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

Разделы

Аффилиация

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