mapDomainEmbedding — Mathlib

English

Defines an embedding mapDomainEmbedding : (α →₀ ℕ) ↪ (β →₀ ℕ) induced by an embedding f : α ↪ β.

Русский

Определяет вложение mapDomainEmbedding : (α →₀ ℕ) ↪ (β →₀ ℕ), индуцированное вложением f : α ↪ β.

LaTeX

$$$$ \mathrm{mapDomainEmbedding}\ {\alpha}\ {\beta}\ (f) : (\alpha \to_\mathbb{N} \!) \hookrightarrow (\beta \to_\mathbb{N} \!). $$$$

Lean4

/-- When `f` is an embedding we have an embedding `(α →₀ ℕ) ↪ (β →₀ ℕ)` given by `mapDomain`. -/
@[simps]
def mapDomainEmbedding {α β : Type*} (f : α ↪ β) : (α →₀ ℕ) ↪ β →₀ ℕ :=
  ⟨Finsupp.mapDomain f, Finsupp.mapDomain_injective f.injective⟩

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