ι_image_le

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Opens.ι_image_le

English

Image of ι respects the lattice order on opens.

Русский

Изображение ι сохраняет порядок подмножеств в решетке открытых множеств.

LaTeX

$$ι_image_le (W) : U.ι ''ᵁ W ≤ U$$

Lean4

theorem ι_image_le (W : U.toScheme.Opens) : U.ι ''ᵁ W ≤ U :=
  by
  simp_rw [← U.ι_image_top]
  exact U.ι.image_le_image_of_le le_top

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

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

Разделы

Аффилиация

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