MapsTo — Mathlib

English

MapsTo f s t means that the image of s is contained in t: ∀ x ∈ s, f(x) ∈ t.

Русский

MapsTo f s t означает, что образ s содержится в t: ∀ x ∈ s, f(x) ∈ t.

LaTeX

$$$$\\mathrm{MapsTo}(f,s,t) \\;\\Longleftrightarrow\\; \\forall x\\,(x\\in s \\rightarrow f(x) \\in t).$$$$

Lean4

/-- `MapsTo f s t` means that the image of `s` is contained in `t`. -/
def MapsTo (f : α → β) (s : Set α) (t : Set β) : Prop :=
  ∀ ⦃x⦄, x ∈ s → f x ∈ t

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