core_def

Mathlib.Data.PFun

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

English

Equivalently, the core is the set of x where f(x) is a subset of s.

Русский

Эквивалентно ядро — это множество x, для которых f(x) ⊆ s.

LaTeX

$$$f.core\\,s = \\{ x : \\alpha \\mid \\forall y,\\ y \\in f(x) \\rightarrow y \\in s \\}$$$

Lean4

theorem core_def (s : Set β) : f.core s = {x | ∀ y, y ∈ f x → y ∈ s} :=
  rfl

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

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

Разделы

Аффилиация

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