resLE_comp_ι — Mathlib

English

Restriction of f commutes with inclusions of open subsets: composing with ι on the target side equals restricting after applying ι to the source side.

Русский

Ограничение f коммутирует с включениями открытых подмножеств: композиция с ι слева равна ограничению после применения ι к источнику.

LaTeX

$$$(f.resLE U V e) \;\circ U.\iota = V.\iota \circ f$$$

Lean4

@[reassoc (attr := simp)]
theorem resLE_comp_ι : f.resLE U V e ≫ U.ι = V.ι ≫ f := by simp [resLE]

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