inv — Mathlib

English

Let α be a type with an involution inv: α → α such that inv(inv(x)) = x. If f is a nontrivial (i.e., not bottom) filter on α, then the inverse filter f^{-1} is also nontrivial.

Русский

Пусть α обладает инволютивной операцией inv: α → α, такая что inv(inv(x)) = x. Тогда для любого непустого (не нижнего) фильтра f на α обратный фильтр f^{-1} также непустой.

LaTeX

$$$$ \forall \alpha\ [Inv\alpha], \forall f : \mathcal{F}(\alpha), f \neq \bot \Rightarrow f^{-1} \neq \bot. $$$$

Lean4

@[to_additive]
protected theorem inv : f.NeBot → f⁻¹.NeBot := fun h => h.map _

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