core_subset_core

Mathlib.Data.Rel

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

English

If t1 is contained in t2, then the core of t1 is contained in the core of t2 with respect to R.

Русский

Если t1 ⊆ t2, то ядро t1 относится к ядру t2 по отношению R с сохранением подмножеств.

LaTeX

$$$R.core(t_1) \subseteq R.core(t_2)$$$

Lean4

@[gcongr]
theorem core_subset_core (ht : t₁ ⊆ t₂) : R.core t₁ ⊆ R.core t₂ := fun _a ha _b hab ↦ ht <| ha hab

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

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

Разделы

Аффилиация

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