English
The core of s can be expressed as the union of the preimage of s and the complement of the domain: f.core(s) = f.preimage(s) ∪ Dom(f)ᶜ.
Русский
Ядро множества s можно выразить как объединение предобраза s и комплемента области определения: f.core(s) = f.preimage(s) ∪ Dom(f)ᶜ.
LaTeX
$$$$ f.core(s) = f.preimage(s) \cup \mathrm{Dom}(f)^{\mathrm{c}}. $$$$
Lean4
theorem core_eq (f : α →. β) (s : Set β) : f.core s = f.preimage s ∪ f.Domᶜ := by
rw [preimage_eq, Set.inter_union_distrib_right, Set.union_comm (Dom f), Set.compl_union_self, Set.inter_univ,
Set.union_eq_self_of_subset_right (f.compl_dom_subset_core s)]
