English
For a partial function f, the preimage of s under f is equal to the intersection of the core of s and the domain of f: f.preimage s = f.core s ∩ f.Dom.
Русский
Для частичной функции f предобраз множества s равен пересечению ядра s и области определения: f.preimage s = f.core s ∩ f.Dom.
LaTeX
$$$$ f.preimage(s) = f.core(s) \cap f.Dom. $$$$
Lean4
theorem preimage_eq (f : α →. β) (s : Set β) : f.preimage s = f.core s ∩ f.Dom :=
Set.eq_of_subset_of_subset (Set.subset_inter (f.preimage_subset_core s) (f.preimage_subset_dom s))
fun x ⟨xcore, xdom⟩ =>
let y := (f x).get xdom
have ys : y ∈ s := xcore (Part.get_mem _)
show x ∈ f.preimage s from ⟨(f x).get xdom, ys, Part.get_mem _⟩
