subtypeInjectiveEquivEmbedding — Mathlib

English

There is a natural bijection between the type of embeddings α ↪ β and the set of injective maps α → β.

Русский

Существуют естественная биекция между типом вложений α ↪ β и множеством инъективных отображений α → β.

LaTeX

$$$\\{ f : \\alpha \\to \\beta \\,\\mid\\, \\operatorname{Injective}(f) \\} \\simeq (\\alpha \\hookrightarrow \\beta)$$$

Lean4

/-- The type of embeddings `α ↪ β` is equivalent to
the subtype of all injective functions `α → β`. -/
def subtypeInjectiveEquivEmbedding (α β : Sort*) : { f : α → β // Injective f } ≃ (α ↪ β)
    where
  toFun f := ⟨f.val, f.property⟩
  invFun f := ⟨f, f.injective⟩

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