basicOpen_le

Mathlib.Geometry.RingedSpace.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.RingedSpace.basicOpen_le

English

BasicOpen is contained in the ambient open that generated it.

Русский

BasicOpen вложено в исходное открытое пространство.

LaTeX

$$$BasicOpen(f) \le U$$$

Lean4

theorem basicOpen_le {U : Opens X} (f : X.presheaf.obj (op U)) : X.basicOpen f ≤ U := by rintro x ⟨h, _⟩; exact h

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

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

Разделы

Аффилиация

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