English
Let f be a partial function f: α →. β and s a subset of β. An element x ∈ α lies in the core of s with respect to f precisely when every value produced by f at x lies in s. Equivalently, f(x) is contained in s.
Русский
Пусть f — частичная функция f: α →. β и s ⊆ β. Элемент x ∈ α принадлежит ядру s по отношению к f тогда и только тогда каждый элемент, который даёт f при x, принадлежит s. Иными словами, образ f(x) ⊆ s.
LaTeX
$$$$ x \in f.core(s) \;\iff\; \forall y\,(y \in f(x) \rightarrow y \in s) $$$$
Lean4
@[simp]
theorem mem_core (x : α) (s : Set β) : x ∈ f.core s ↔ ∀ y, y ∈ f x → y ∈ s :=
Iff.rfl
