app_eq_appLE — Mathlib

English

For any open U in Y, the morphism app at U equals the appLE map with the corresponding preimage; that is f.app U = f.appLE U ((TopologicalSpace.Opens.map f.base).obj U) le_rfl.

Русский

Для любого открытого множества U в Y: f.app U = f.appLE U ((образ подмножеством по основанию f.base).obj U) le_rfl.

LaTeX

$$$f.app U = f.appLE U \\big( (\\mathrm{TopologicalSpace.Opens.map} \\; f.base).obj\\; U \\big) \\; \\text{le}_\\mathrm{rfl}$$$

Lean4

theorem app_eq_appLE {U : Y.Opens} : f.app U = f.appLE U _ le_rfl := by simp [Hom.appLE]

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