image_preimage_eq_opensRange_inter

Mathlib.AlgebraicGeometry.OpenImmersion

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

← MathLib Explorer

English

For U open in Y, the image of the preimage of U is the intersection of f.opensRange with U.

Русский

Для открытого U в Y образ предобраза U по f равен пересечению f.opensRange с U.

LaTeX

$$$f ''ᵁ (f^{-1}^ᵁ U) = f.opensRange \\cap U$$$

Lean4

theorem image_preimage_eq_opensRange_inter (U : Y.Opens) : f ''ᵁ f ⁻¹ᵁ U = f.opensRange ⊓ U :=
  by
  apply Opens.ext
  simp [Set.image_preimage_eq_range_inter]

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

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

Разделы

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

Аффилиация

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