comap_inv — Mathlib

English

Let α have an involutive inversion inv: α → α. For any filter f on α, the preimage of f under inv equals the inverse filter, i.e., comap inv f = f^{-1}.

Русский

Пусть на α определена инволюционная операция обращения inv: α → α. Для любого фильтра f на α предобраз по inv равен обратному фильтру: comap inv f = f^{-1}.

LaTeX

$$$$ \operatorname{comap}_{Inv.inv}(f) = f^{-1}. $$$$

Lean4

@[to_additive (attr := simp)]
protected theorem comap_inv : comap Inv.inv f = f⁻¹ :=
  .symm <| map_eq_comap_of_inverse (inv_comp_inv _) (inv_comp_inv _)

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