comp_antitone — Mathlib

English

If f is maximal on s at a, then for any antitone g, g∘f is minimal on s on a.

Русский

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

LaTeX

$$$\text{IsMaxOn}(f,s,a) \rightarrow \text{Antitone}(g) \rightarrow \text{IsMinOn}(g\circ f,s,a)$$$

Lean4

theorem comp_antitone (hf : IsMaxFilter f l a) {g : β → γ} (hg : Antitone g) : IsMinFilter (g ∘ f) l a :=
  hf.dual.comp_mono fun _ _ h => hg h

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