comp_mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_mono (hf : IsMaxFilter f l a) {g : β → γ} (hg : Monotone g) : IsMaxFilter (g ∘ f) l a :=
  mem_of_superset hf fun _x hx => hg hx

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