basicOpen_mono

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Proj.basicOpen_mono

English

If f divides g, then basicOpen 𝒜 g ≤ basicOpen 𝒜 f.

Русский

Если f делит g, то D₊(g) ⊆ D₊(f).

LaTeX

$$basicOpen 𝒜 g ≤ basicOpen 𝒜 f$$

Lean4

theorem basicOpen_mono (hfg : f ∣ g) : basicOpen 𝒜 g ≤ basicOpen 𝒜 f :=
  (hfg.choose_spec ▸ basicOpen_mul 𝒜 f _).trans_le inf_le_left

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

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

Разделы

Аффилиация

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