isConnected_of_lowerHalfPlane — Mathlib

English

If the set s contains the open lower half-plane { z ∈ ℂ : Im z < r } and is contained in the closed half-plane { z ∈ ℂ : Im z ≤ r }, then s is connected.

Русский

Если множество s содержит открытую нижнюю полуплоскость { z ∈ ℂ : Im z < r } и помещается внутри замкнутой полуплоскости { z ∈ ℂ : Im z ≤ r }, то s связано.

LaTeX

$$Если r ∈ ℝ и { z ∈ ℂ : Im z < r } ⊆ s ⊆ { z ∈ ℂ : Im z ≤ r }, то s является связным.$$

Lean4

theorem isConnected_of_lowerHalfPlane {r} {s : Set ℂ} (hs₁ : {z | z.im < r} ⊆ s) (hs₂ : s ⊆ {z | z.im ≤ r}) :
    IsConnected s := by
  refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_im_lt] using hs₂)
  exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩

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