English
For an ordered monoid G, the comap of the top filter along the magnitude map mabs is the join of the bottom and the top filters: comap(mabs, atTop) = atBot ⊔ atTop.
Русский
Для упорядоченного моноида G прообраз фильтра «вверх» по отображению величины mabs равен объединению нижнего и верхнего фильтров: comap(mabs, atTop) = atBot ⊔ atTop.
LaTeX
$$$\\operatorname{comap}(\\mathrm{mabs}: G \\to G)(\\operatorname{atTop}) = \\operatorname{atBot} \\sqcup \\operatorname{atTop}$$$
Lean4
@[to_additive (attr := simp)]
theorem comap_mabs_atTop [IsOrderedMonoid G] : comap (mabs : G → G) atTop = atBot ⊔ atTop :=
by
refine
le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
(sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)
rintro ⟨a, b⟩ -
refine ⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩
rw [mem_preimage, mem_Ici, le_mabs', max_le_iff, ← min_inv_inv', le_min_iff, inv_inv] at hx
exact hx.imp And.left And.right
