subset_verticalStrip_of_isCompact

English

If K ⊆ ℍ is compact, then there exist A,B with B>0 such that K ⊆ verticalStrip(A,B).

Русский

Пусть K ⊆ ℍ компактно. Тогда существуют A,B с B>0 такие, что K ⊆ verticalStrip(A,B).

LaTeX

$$∀ {K ⊆ ℍ}, IsCompact K ⇒ ∃ A,B ∈ ℝ, 0 < B ∧ K ⊆ verticalStrip(A,B).$$

Lean4

theorem subset_verticalStrip_of_isCompact {K : Set ℍ} (hK : IsCompact K) : ∃ A B : ℝ, 0 < B ∧ K ⊆ verticalStrip A B :=
  by
  rcases K.eq_empty_or_nonempty with rfl | hne
  · exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩
  obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn
  obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn
  exact ⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩

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