toOpens_mono

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono

Lean4

theorem toOpens_mono : Monotone (toOpens (X := X)) :=
  by
  rintro ⟨U, hU⟩ ⟨V, hV⟩ ⟨f, rfl⟩
  exact X.basicOpen_le _

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

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

Разделы

Аффилиация

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