isConnected_of_upperHalfPlane — Mathlib

English

If a set s contains the open upper 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 ∈ ℝ и s ⊆ ℂ удовлетворяют { z ∈ ℂ : Im z > r } ⊆ s ⊆ { z ∈ ℂ : Im z ≥ r }, то s является связным.$$

Lean4

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

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