subtypeEmb — Mathlib

English

If de : IsDenseEmbedding e, then IsDenseEmbedding.subtypeEmb p e is an IsDenseEmbedding.

Русский

Если de : IsDenseEmbedding e, то IsDenseEmbedding.subtypeEmb p e — плотное вложение.

LaTeX

$$$IsDenseEmbedding.subtype\\ e \\Rightarrow IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)$$$

Lean4

/-- The dense embedding of a subtype inside its closure. -/
@[simps]
def subtypeEmb {α : Type*} (p : α → Prop) (e : α → β) (x : { x // p x }) : { x // x ∈ closure (e '' {x | p x}) } :=
  ⟨e x, subset_closure <| mem_image_of_mem e x.prop⟩

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