isLocalHomeomorph_coe — Mathlib

English

Under densely ordered and 0<p, the coercion map is a local homeomorphism from 𝕜 to AddCircle p.

Русский

При плотной упорядоченности и 0<p отображение коэфицирования является локальным гомеоморфизмом из 𝕜 в AddCircle p.

LaTeX

$$$$ \text{IsLocalHomeomorph } (\uparrow) : 𝕜 \to AddCircle\ p $$$$

Lean4

theorem isLocalHomeomorph_coe [DiscreteTopology (zmultiples p)] [DenselyOrdered 𝕜] :
    IsLocalHomeomorph ((↑) : 𝕜 → AddCircle p) := by
  intro a
  obtain ⟨b, hb1, hb2⟩ := exists_between (sub_lt_self a hp.out)
  exact ⟨openPartialHomeomorphCoe p b, ⟨hb2, lt_add_of_sub_right_lt hb1⟩, rfl⟩

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