filter_inf — Mathlib

English

If a is extremal for f with respect to l, then for any l', a is extremal for f with respect to l ⊓ l'.

Русский

Если a является экстремальной точкой для f относительно l, то для любого l' a остается экстремальной точкой для f относительно l ⊓ l'.

LaTeX

$$$\text{IsExtrFilter}(f,l,a) \rightarrow \text{IsExtrFilter}(f,l\,\inf\,l',a)$$$

Lean4

theorem filter_inf (h : IsExtrFilter f l a) (l') : IsExtrFilter f (l ⊓ l') a :=
  h.filter_mono inf_le_left

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