basicOpen_mul_le_left

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

URI: https://scilib.ai/kg/mathlib#ProjectiveSpectrum.basicOpen_mul_le_left

English

The basic open of a product is contained in the basic open of the left factor: basicOpen 𝒜(fg) ⊆ basicOpen 𝒜 f.

Русский

BasicOpen(fg) ⊆ BasicOpen(f).

LaTeX

$$$\mathrm{basicOpen}_{\mathcal{A}}(f\,g) \le \mathrm{basicOpen}_{\mathcal{A}}(f)$$$

Lean4

theorem basicOpen_mul_le_left (f g : A) : basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f :=
  by
  rw [basicOpen_mul 𝒜 f g]
  exact inf_le_left

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

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

Разделы

Аффилиация

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