instInvolutiveInv — Mathlib

English

Inversion on filters is involutive: applying inversion twice yields the original filter, i.e., (f^{-1})^{-1} = f.

Русский

Инверсия над фильтрами является инволюцией: применение инверсии дважды даёт исходный фильтр, то есть (f^{-1})^{-1} = f.

LaTeX

$$$$ (f^{-1})^{-1} = f. $$$$

Lean4

/-- Inversion is involutive on `Filter α` if it is on `α`. -/
@[to_additive /-- Negation is involutive on `Filter α` if it is on `α`. -/
    ]
protected def instInvolutiveInv : InvolutiveInv (Filter α) :=
  { Filter.instInv with inv_inv := fun f => map_map.trans <| by rw [inv_involutive.comp_self, map_id] }

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