resLE_eq_morphismRestrict — Mathlib

English

For a morphism f: X → Y and an open set U ⊆ Y, the restriction of f to U through the preimage U is equal to the canonical restriction morphism from f to U.

Русский

Для морфизма f: X → Y и открытого множества U ⊆ Y ограничение f на U через его прообраз совпадает с каноническим ограничением самого f на U.

LaTeX

$$$f.resLE\;U\;(f^{-1}\!U)\;\mathrm{le\_rfl} = f\mid_U$$$

Lean4

theorem resLE_eq_morphismRestrict : f.resLE U (f ⁻¹ᵁ U) le_rfl = f ∣_ U := by simp [resLE]

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