atImInfty_mem — Mathlib

English

For any subset S of the upper half-plane, S belongs to atImInfty iff there exists a real A such that z ∈ S whenever Im z ≥ A.

Русский

Для любой подмножества S верхней полуплоскости верно: S ∈ atImInfty тогда и только тогда, когда существует число A ∈ ℝ такое, что z ∈ S при условии, что Im z ≥ A.

LaTeX

$$$S \in \text{atImInfty} \iff \exists A \in \mathbb{R}, \forall z \in \mathbb{H}, A \le \operatorname{im}(z) \Rightarrow z \in S$$$

Lean4

theorem atImInfty_mem (S : Set ℍ) : S ∈ atImInfty ↔ ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → z ∈ S := by
  simp only [atImInfty_basis.mem_iff, true_and]; rfl

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