imageFactorization — Mathlib

English

Restriction of f to s factors through the image: there is a map imageFactorization f s : s → f''s given by p ↦ ⟨f p.1, mem_image_of_mem f p.2⟩.

Русский

Ограничение f до s факторизуется через образ, задавая отображение imageFactorization f s : s → f''s так, что p ↦ ⟨f p.1, доказательство, что f p.1 ∈ f''s⟩.

LaTeX

$$$\\mathrm{imageFactorization}(f,s) : s \\to f''s$,\\quad $(p) \\mapsto \\langle f(p_1), \\mathrm{mem\\_image\\_of\\_mem} f p_2 \\rangle$$$

Lean4

/-- Restriction of `f` to `s` factors through `s.imageFactorization f : s → f '' s`. -/
def imageFactorization (f : α → β) (s : Set α) : s → f '' s := fun p => ⟨f p.1, mem_image_of_mem f p.2⟩

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