English
For a relation R between α and β and a subset S ⊆ β, the core of S with respect to R is the set of a ∈ α such that every b with a R b lies in S.
Русский
Для отношения R между α и β и подмножества S ⊆ β ядро S относительно R есть множество элементов a ∈ α такие, что каждое b, связанный с a через R, лежит в S.
LaTeX
$$$\\mathrm{core}_R(S) = \\{ a \\in \\alpha \\mid \\forall b,\\ a \\mathrel{R} b \\Rightarrow b \\in S\\}$$$
Lean4
/-- Core of a set `S : Set β` w.R.t `R : SetRel α β` is the set of `x : α` that are related *only*
to elements of `S`. Other generalization of `Function.preimage`. -/
def core : Set α :=
{a | ∀ ⦃b⦄, a ~[R] b → b ∈ t}
