range_restrictPreimage — Mathlib

English

The range of the preimage-restriction map t.restrictPreimage f equals the preimage under the projection val of the range of f.

Русский

Образ отображения типа preimage с ограничением по t равен предобразу по проекции Val от образа функции f.

LaTeX

$$$\operatorname{range}(t.restrictPreimage f) = \operatorname{val}^{-1}(\operatorname{range}(f))$$$

Lean4

theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.val ⁻¹' range f := by
  simp only [← image_univ, ← image_restrictPreimage, preimage_univ]

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