English
The determinant of conjLIE considered as a linear equivalence is −1.
Русский
Детерминант conjLIE, как линейное биеканальное отображение, равен −1.
LaTeX
$$$\\operatorname{det}(\\text{conjLIE}^{\\text{toLinearEquiv}}) = -1$$$
Lean4
/-- The *open mapping theorem* for holomorphic functions, global version: if a function `g : E → ℂ`
is analytic on a connected set `U`, then either it is constant on `U`, or it is open on `U` (in the
sense that it maps any open set contained in `U` to an open set in `ℂ`). -/
theorem is_constant_or_isOpen (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) :
(∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s) :=
by
by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
· obtain ⟨z₀, hz₀, h⟩ := h
exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩
· push_neg at h
refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_
rintro z ⟨w, hw1, rfl⟩
exact
(hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
(image_mem_map (hs2.mem_nhds hw1))
