verticalStrip_mono

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.verticalStrip_mono

← MathLib Explorer

English

If A ≤ A' and B' ≤ B then verticalStrip(A,B) ⊆ verticalStrip(A',B').

Русский

Если A ≤ A' и B' ≤ B, то verticalStrip(A,B) ⊆ verticalStrip(A',B').

LaTeX

$$A ≤ A' ∧ B' ≤ B ⇒ verticalStrip(A,B) ⊆ verticalStrip(A',B').$$

Lean4

@[gcongr]
theorem verticalStrip_mono {A B A' B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) : verticalStrip A B ⊆ verticalStrip A' B' :=
  by
  rintro z ⟨hzre, hzim⟩
  exact ⟨hzre.trans hA, hB.trans hzim⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru