coe_preimage — Mathlib

English

The preimage defined for a lifted function coincides with the standard preimage for the underlying function.

Русский

Предобраз для подстановки лейфтовой функции совпадает со стандартным предобразом соответствующей функции.

LaTeX

$$$((f : \\alpha \\to. \\beta).preimage s) = (f : \\alpha \\to \\beta)^{-1}(s)$$$

Lean4

theorem coe_preimage (f : α → β) (s : Set β) : (f : α →. β).preimage s = f ⁻¹' s := by ext; simp

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