isEmbedding_graph

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#isEmbedding_graph

English

If f: X → Y is continuous, then the map x ↦ (x, f(x)) is an embedding.

Русский

Если f: X → Y непрерывно, то отображение x ↦ (x, f(x)) является вложением.

LaTeX

$$$\mathrm{Continuous}(f) \Rightarrow \IsEmbedding(\lambda x: X, (x, f(x)))$$$

Lean4

theorem isEmbedding_graph {f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x) :=
  .of_comp (continuous_id.prodMk hf) continuous_fst .id

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

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

Разделы

Аффилиация

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