le_iff_forall_inf_principal_compl

English

Let f and g be filters on α. Then f ≤ g if and only if for every V in g, the infimum of f with the principal filter on V^c equals the bottom filter.

Русский

Пусть f и g — фильтры на α. Тогда f ≤ g тогда и только тогда, когда для каждого V ∈ g их векторный предел с главной фильтром по V^c равен нулю (нижнему фильтру).

LaTeX

$$$ f \le g \iff \forall V \in g,\ f \wedge \mathcal{P}(V^c) = \bot $$$

Lean4

theorem le_iff_forall_inf_principal_compl {f g : Filter α} : f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
  forall₂_congr fun _ _ => mem_iff_inf_principal_compl

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