surjective_mapsTo_image_restrict — Mathlib

English

For every f and S ⊆ A, the restricted map from S to f[S] is surjective onto f[S]. Equivalently, every element of f[S] has a preimage in S.

Русский

Для каждого f и S ⊆ A ограниченное отображение из S на f[S] сюръективно на f[S]. То есть каждый элемент f(S) имеет предобраз в S.

LaTeX

$$$\forall y \in f''S, \exists x \in S \text{ such that } f(x) = y$$$

Lean4

theorem surjective_mapsTo_image_restrict (f : α → β) (s : Set α) :
    Surjective ((mapsTo_image f s).restrict f s (f '' s)) := fun ⟨_, x, hs, hxy⟩ => ⟨⟨x, hs⟩, Subtype.ext hxy⟩

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