openPartialHomeomorphCoe — Mathlib

English

The open partial homeomorphism structure of the quotient map is compatible with the coe map.

Русский

Структура открытого частичного гомеоморфа совместима с отображением на коэффициент.

LaTeX

$$$$ \text{openPartialHomeomorphCoe is compatible with } (↑) $$$$

Lean4

/-- The quotient map `𝕜 → AddCircle p` as an open partial homeomorphism. -/
@[simps]
def openPartialHomeomorphCoe [DiscreteTopology (zmultiples p)] : OpenPartialHomeomorph 𝕜 (AddCircle p)
    where
  toFun := (↑)
  invFun := fun x ↦ equivIco p a x
  source := Ioo a (a + p)
  target := {↑a}ᶜ
  map_source' := by
    intro x hx hx'
    exact
      hx.1.ne'
        ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx) (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx')
  map_target' := by
    intro x hx
    exact
      (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left
        (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _)
  left_inv' := fun x hx ↦ congrArg _ ((equivIco p a).apply_symm_apply ⟨x, Ioo_subset_Ico_self hx⟩)
  right_inv' := fun x _ ↦ (equivIco p a).symm_apply_apply x
  open_source := isOpen_Ioo
  open_target := isOpen_compl_singleton
  continuousOn_toFun := (AddCircle.continuous_mk' p).continuousOn
  continuousOn_invFun := by
    exact continuousOn_of_forall_continuousAt (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a)

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