codRestrict — Mathlib

English

Restrict the codomain of an embedding to a subset p whenever the image lies in p.

Русский

Ограничиваем кодом вложение до подмножества p, если образ лежит в p.

LaTeX

$$$\\text{codRestrict } p\, f\, H : \\alpha \\hookrightarrow p.\\!\\mathrm{Elem}$ with $H(a): f(a) \\in p$$$

Lean4

/-- Restrict the codomain of an embedding. -/
def codRestrict {α β} (p : Set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : α ↪ p :=
  ⟨fun a ↦ ⟨f a, H a⟩, fun _ _ h ↦ f.injective (congr_arg Subtype.val h)⟩

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