comp_mono — Mathlib

English

If f is extremal along l at a, and g is monotone, then g∘f is extremal along l at a.

Русский

Если f экстремален вдоль l в a, и g монотонна, то g∘f экстремален вдоль l в a.

LaTeX

$$$\text{IsExtrFilter}(f,l,a) \rightarrow \text{Monotone}(g) \rightarrow \text{IsExtrFilter}(g\circ f,l,a)$$$

Lean4

theorem comp_mono (hf : IsExtrFilter f l a) {g : β → γ} (hg : Monotone g) : IsExtrFilter (g ∘ f) l a :=
  hf.elim (fun hf => (hf.comp_mono hg).isExtr) fun hf => (hf.comp_mono hg).isExtr

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