basicOpen_mul_le_right

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

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

English

Similarly, basicOpen 𝒜(fg) ⊆ basicOpen 𝒜 g.

Русский

Аналогично, BasicOpen(fg) ⊆ BasicOpen(g).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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