core_inter

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.core_inter

English

The core of an intersection is the intersection of cores: f.core(s ∩ t) = f.core(s) ∩ f.core(t).

Русский

Ядро пересечения равно пересечению ядер: f.core(s ∩ t) = f.core(s) ∩ f.core(t).

LaTeX

$$$$ f.core(s \cap t) = f.core(s) \cap f.core(t). $$$$

Lean4

theorem core_inter (s t : Set β) : f.core (s ∩ t) = f.core s ∩ f.core t :=
  SetRel.core_inter _ s t

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

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

Разделы

Аффилиация

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