verticalStrip_anti_right

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

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

English

verticalStrip A B ⊆ verticalStrip A B' if B' ≤ B.

Русский

verticalStrip(A,B) ⊆ verticalStrip(A,B') при B' ≤ B.

LaTeX

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

Lean4

theorem verticalStrip_anti_right (A) {B B'} (h : B' ≤ B) : verticalStrip A B ⊆ verticalStrip A B' :=
  verticalStrip_mono le_rfl h

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

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

Разделы

Аффилиация

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