English
The preimage of the complement of s is the complement of the preimage of s, under appropriate injectivity hypotheses.
Русский
Предобраз дополнения s равно дополнению предобраза s при соответствующих условиях инъективности.
LaTeX
$$$$ \\mathrm{preimage}(s^{\\mathrm{c}}, f, hfc) = (\\mathrm{preimage}(s, f, hf))^{\\mathrm{c}}. $$$$
Lean4
@[simp]
theorem preimage_compl' [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] {f : α → β} (s : Finset β)
(hfc : InjOn f (f ⁻¹' ↑sᶜ)) (hf : InjOn f (f ⁻¹' ↑s)) : preimage sᶜ f hfc = (preimage s f hf)ᶜ :=
Finset.coe_injective
(by simp)
-- Not `@[simp]` since `simp` can't figure out `hf`; `simp`-normal form is `preimage_compl'`.
