English
The preimage of a set under a partial function, when viewed as a subtype-valued function, coincides with the preimage under the underlying function composed with the Subtype.val projection: f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s.
Русский
Предобраз множества под частичной функцией при взгляде на неё как на функцию со значениями-подтипами совпадает с предобразом подлежащей функции через проекцию Subtype.val: f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s.
LaTeX
$$$$ f.asSubtype^{-1}(s) = (\mathrm{Subtype}.val)^{-1}(f.preimage(s)). $$$$
Lean4
theorem preimage_asSubtype (f : α →. β) (s : Set β) : f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s :=
by
ext x
simp only [Set.mem_preimage, PFun.asSubtype, PFun.mem_preimage]
show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
exact
Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
Part.mem_unique fxy this ▸ ys
