asEmbedding — Mathlib

English

Given e: α ≃ Subtype p, produce an embedding α ↪ β by composing e with the natural inclusion of Subtype p into β.

Русский

Заданному e: α ≃ Subtype p построить вложение α ↪ β путём композиции с естественным включением Subtype p в β.

LaTeX

$$$\\mathrm{asEmbedding}(e): \\alpha \\hookrightarrow \\beta$$$

Lean4

/-- Given an equivalence to a subtype, produce an embedding to the elements of the corresponding
set. -/
@[simps!]
def asEmbedding {β α : Sort*} {p : β → Prop} (e : α ≃ Subtype p) : α ↪ β :=
  e.toEmbedding.trans (subtype p)

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