image — Mathlib

English

The image map sends an embedding f to an embedding on sets, preserving injectivity.

Русский

Образ отображения передаётся в вложение между множествами, сохраняющее инъективность.

LaTeX

$$$\\text{Function.Embedding.image } f : \\mathcal{Set} \\;\\hookrightarrow \\mathcal{Set}$ with $\\operatorname{toFun}(f) = \\mathrm{image}(f)$ and $\\operatorname{inj}'$$$

Lean4

/-- `Set.image` as an embedding `Set α ↪ Set β`. -/
@[simps apply]
protected def image {α β} (f : α ↪ β) : Set α ↪ Set β :=
  ⟨image f, f.2.image_injective⟩

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