coe_preimage — Mathlib

English

When viewed as a set, the preimage Finset corresponds exactly to the standard set-theoretic preimage.

Русский

При восприятии как множества предобраз Finset совпадает с обычным множество‑предобразом.

LaTeX

$$$$ \\bigl( \\mathrm{preimage}(s,f,hf) \\bigr)^{\\!\\mathrm{toSet}} = f^{-1}(s). $$$$

Lean4

@[simp, norm_cast]
theorem coe_preimage {f : α → β} (s : Finset β) (hf : Set.InjOn f (f ⁻¹' ↑s)) :
    (↑(preimage s f hf) : Set α) = f ⁻¹' ↑s :=
  Set.Finite.coe_toFinset _

Похожие утверждения