isIso_app

Mathlib.AlgebraicGeometry.OpenImmersion

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

← MathLib Explorer

English

If V is a subset of opensRange, then f.app(V) is an isomorphism.

Русский

Если V⊆opensRange, то f.app(V) — изоморфизм.

LaTeX

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

Lean4

theorem isIso_app (V : Y.Opens) (hV : V ≤ f.opensRange) : IsIso (f.app V) :=
  by
  rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]
  infer_instance

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

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

Разделы

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

Аффилиация

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