toOpens_injective

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

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

English

The basicOpen map from an affine site to opens is injective on opens.

Русский

Базовое открытое отображение инжектирует виды открытых подмножеств.

LaTeX

$$Function.Injective (toOpens (X := X))$$

Lean4

theorem toOpens_injective : Function.Injective (toOpens (X := X)) :=
  Subtype.val_injective

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

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

Разделы

Аффилиация

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