core_mono

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.core_mono

English

The core operator R.core is monotone: it preserves inclusions of target sets.

Русский

Оператор ядра R.core is сохраняет включения множеств-образов.

LaTeX

$$Monotone$R.\mathrm{core}$$$

Lean4

theorem core_mono : Monotone R.core := fun _ _ ↦ core_subset_core

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

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

Разделы

Аффилиация

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