rangeRestrict_surjective — Mathlib

English

The range-restriction f.rangeRestrict is surjective: every element of f.range has a preimage in R.

Русский

Ограничение образа по f является сурьективным: любой элемент образа f имеет дообразование в R.

LaTeX

$$$ \text{Surjective}(f.rangeRestrict) $$$

Lean4

theorem rangeRestrict_surjective (f : R →+* S) : Function.Surjective f.rangeRestrict := fun ⟨_y, hy⟩ =>
  let ⟨x, hx⟩ := mem_range.mp hy
  ⟨x, Subtype.ext hx⟩

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