comap_inf_principal_neBot_of_image_mem

English

If m''s ∈ g, then the infimum of comap m g and principal s is nontrivial.

Русский

Если m''s принадлежит g, то инфимум (comap m g) ∩ (principal s) не тривиален.

LaTeX

$$$m''s \\in g \\Rightarrow (\\operatorname{comap} m\,g \\cap \\mathcal{P}s) \\text{ is NeBot}$$$

Lean4

theorem comap_inf_principal_neBot_of_image_mem (h : m '' s ∈ g) : (Filter.comap m g ⊓ 𝓟 s).NeBot :=
  Filter.comap_inf_principal_neBot_of_image_mem g.neBot h

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