instInv — Mathlib

English

There is an inverse operation on filters defined by f⁻¹ := map Inv.inv, i.e., the filter obtained by preimages under inversion.

Русский

Существуют операции обращения над фильтрами, определяемые как f⁻¹ := map Inv.inv, то есть фильтр, получаемый взвешиванием через инверсию.

LaTeX

$$$f^{-1} := \\mathrm{map}(Inv.inv, f)$$$

Lean4

/-- The inverse of a filter is the pointwise preimage under `⁻¹` of its sets. -/
@[to_additive /-- The negation of a filter is the pointwise preimage under `-` of its sets. -/
    ]
instance instInv : Inv (Filter α) :=
  ⟨map Inv.inv⟩

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