filter_mono — Mathlib

English

If f is extremal with respect to a filter l at a and l' is a finer filter than l, then f is extremal with respect to l' at a as well.

Русский

Если f имеет крайнее значение относительно фильтра l в точке a, и l' является более тонким фильтром по сравнению с l, то в точке a f сохраняет крайнее значение по l'.

LaTeX

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

Lean4

theorem filter_mono (h : IsExtrFilter f l a) (hl : l' ≤ l) : IsExtrFilter f l' a :=
  h.elim (fun h => (h.filter_mono hl).isExtr) fun h => (h.filter_mono hl).isExtr

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