atImInfty_basis — Mathlib

English

The atImInfty filter has a basis given by preimages of rays [i, ∞) under the imaginary part.

Русский

У фильтра atImInfty есть базис, задаваемый предобразами множеств [i, ∞) по мнимой части.

LaTeX

$$$\text{atImInfty}.HasBasis(\lambda \_ => \text{True}, \lambda i : \mathbb{R}, \operatorname{im}^{-1}([i,\infty)))$$$

Lean4

theorem atImInfty_basis : atImInfty.HasBasis (fun _ => True) fun i : ℝ => im ⁻¹' Set.Ici i :=
  Filter.HasBasis.comap UpperHalfPlane.im Filter.atTop_basis

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