cobounded_eq — Mathlib

English

The cobounded filter on ℤ equals the join of the bottom and top filters.

Русский

Замкованный по границам фильтр на \mathbb{Z} равен объединению нижнего и верхнего фильтров.

LaTeX

$$$\operatorname{cobounded}(\mathbb{Z}) = \operatorname{atBot} \sqcup \operatorname{atTop}$$$

Lean4

@[simp]
theorem cobounded_eq : Bornology.cobounded ℤ = atBot ⊔ atTop := by
  simp_rw [← comap_dist_right_atTop (0 : ℤ), dist_eq', sub_zero, ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ,
    comap_comap];
  rfl

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