English
Let f be a partial function and s ⊆ α, t ⊆ β. The membership x ∈ (res f s).core t is equivalent to x ∈ s implies f(x) ∈ t. This describes how restricting the domain influences core membership.
Русский
Пусть f — частичная функция и s ⊆ α, t ⊆ β. Членство x ∈ (res f s).core t эквивалентно тому, что если x ∈ s, то f(x) ∈ t. Это описывает влияние ограничения области определения на членство в ядре.
LaTeX
$$$$ x \in (\mathrm{res}(f,s)).core(t) \;\iff\; x \in s \;\rightarrow\; f(x) \in t. $$$$
Lean4
theorem mem_core_res (f : α → β) (s : Set α) (t : Set β) (x : α) : x ∈ (res f s).core t ↔ x ∈ s → f x ∈ t := by
simp [mem_core, mem_res]
