SurjOn — Mathlib

English

Let f: α → β, s ⊆ α, t ⊆ β. Then t is contained in the image of s under f, i.e., t ⊆ f''s.

Русский

Пусть f: α → β, s ⊆ α, t ⊆ β. Тогда t содержится в образе s под действием f, то есть t ⊆ f[s].

LaTeX

$$$\mathrm{SurjOn}(f,s,t) \iff t \subseteq f''s$$$

Lean4

/-- `f` is surjective from `s` to `t` if `t` is contained in the image of `s`. -/
def SurjOn (f : α → β) (s : Set α) (t : Set β) : Prop :=
  t ⊆ f '' s

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