restrictPreimage — Mathlib

English

The restriction of a function onto the preimage of a set: t ⊆ β, restrictPreimage(t,f): f⁻¹' t → t maps x ↦ f(x).

Русский

Ограничение функции на предобразе множества: restrictPreimage(t,f): f⁻¹' t → t действует как x ↦ f(x).

LaTeX

$$$$\\text{restrictPreimage }(t,f): (f^{-1}' t) \\to t,\\; x \\mapsto f(x).$$$$

Lean4

/-- The restriction of a function onto the preimage of a set. -/
@[simps!]
def restrictPreimage (t : Set β) (f : α → β) : f ⁻¹' t → t :=
  (Set.mapsTo_preimage f t).restrict _ _ _

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