preimage_image_eq

Mathlib.AlgebraicGeometry.OpenImmersion

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

← MathLib Explorer

English

If V is contained in f.opensRange, then f.app(V) is an isomorphism.

Русский

Если V вложено в f.opensRange, то f.app(V) является изоморфизмом.

LaTeX

$$$\\text{If } V \\le f.opensRange, \\text{ then } f.app(V) \\text{ is an isomorphism.}$$$

Lean4

@[simp]
theorem preimage_image_eq (U : X.Opens) : f ⁻¹ᵁ f ''ᵁ U = U :=
  by
  apply Opens.ext
  simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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