eventuallyEq_coe_comp_ofComplex — Mathlib

English

Let z ∈ ℂ have positive imaginary part. The composition UpperHalfPlane.coe ∘ ofComplex agrees with the identity function in a neighborhood of z; i.e., there exists a neighborhood of z on which the composed map equals the identity.

Русский

Пусть z ∈ ℂ с положительной мнимой частью. Композиция UpperHalfPlane.coe ∘ ofComplex совпадает с тождественной функцией в окрестности z; существует окрестность z, на которой полученная композиция равна тождественной отображению.

LaTeX

$$$\exists U \ni z:\ (\forall w \in U),\ (\text{UpperHalfPlane.coe} \circ \text{ofComplex})(w) = w$$$

Lean4

theorem eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) : UpperHalfPlane.coe ∘ ofComplex =ᶠ[𝓝 z] id :=
  by
  filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds hz] with x hx
  simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq, coe_mk_subtype]

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