inv_atTop — Mathlib

English

In a ordered commutative group G, the inverse of the atTop filter is the atBot filter: (atTop)^{-1} = atBot.

Русский

В упорядоченной абелевой группе G обратный фильтр к atTop равен фильтру atBot: (atTop)^{-1} = atBot.

LaTeX

$$$$ (atTop : Filter\, G)^{-1} = atBot. $$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_atTop {G : Type*} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : (atTop : Filter G)⁻¹ = atBot :=
  (OrderIso.inv G).map_atTop

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