core — Mathlib

English

The core of a set s with respect to f is the set of all a ∈ α such that every y in f(a) lies in s.

Русский

Ядро множества s относительно f — множество всех a ∈ α, для которых каждый y ∈ f(a) принадлежит s.

LaTeX

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

Lean4

/-- Core of a set `s : Set β` with respect to a partial function `f : α →. β`. Set of all `a : α`
such that `f a ∈ s`, if `f a` is defined. -/
def core (s : Set β) : Set α :=
  f.graph'.core s

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