English
The preimage of s under the composition f.comp g equals g.preimage (f.preimage s).
Русский
Предобраз множества s по композиции f ∘ g равен предобразу по g от предобраза s по f.
LaTeX
$$$$ (f.comp g).preimage s = g.preimage (f.preimage s). $$$$
Lean4
@[simp]
theorem preimage_comp (f : β →. γ) (g : α →. β) (s : Set γ) : (f.comp g).preimage s = g.preimage (f.preimage s) :=
by
ext
simp_rw [mem_preimage, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]
rw [exists_comm]
simp_rw [and_assoc, and_comm]