image_subset — Mathlib

English

If A ⊆ B are subsets of α and f: α → β is a function, then the image of A under f is contained in the image of B under f: f[A] ⊆ f[B].

Русский

Если A ⊆ B внутри α и f: α → β, тогда образ A под действием f содержится в образе B: f[A] ⊆ f[B].

LaTeX

$$$ A \\subseteq B \\Rightarrow f[A] \\subseteq f[B]. $$$

Lean4

@[deprecated image_mono (since := "2025-08-01")]
theorem image_subset {a b : Set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b :=
  image_mono h

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