appLE_eq_app

Mathlib.AlgebraicGeometry.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.appLE_eq_app

English

For any open U, the appLE map with V = f^{-1}(U) and the lower bound le_rfl recovers f.app U; i.e., f.appLE U (f^{-1}ᵁ U) le_rfl = f.app U.

Русский

Для открытого U выполняется f.appLE U (f^{-1}ᵁ U) le_rfl = f.app U.

LaTeX

$$$f.appLE U (f^{-1}ᵁ U)\\; le_{rfl} = f.app U$$$

Lean4

theorem appLE_eq_app {U : Y.Opens} : f.appLE U (f ⁻¹ᵁ U) le_rfl = f.app U :=
  (app_eq_appLE f).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru