image_injective

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.image_injective

English

The image of a supremum (iSup) of opens equals the supremum of images of the opens.

Русский

Образ суперположения открытых множест равен суперположению образов этих множеств.

LaTeX

$$$f ''ᵁ (\\bigsqcup_i s_i) = \\bigsqcup_i (f ''ᵁ s_i)$$$

Lean4

theorem image_injective : Function.Injective (f ''ᵁ ·) :=
  by
  intro U V hUV
  simpa using congrArg (f ⁻¹ᵁ ·) hUV

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

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

Разделы

Аффилиация

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