comp_mapsTo — Mathlib

English

If hf: IsMaxOn f s a and hg: MapsTo g t s and ha: g b = a, then IsMaxOn (f ∘ g) t b; this follows by dualizing the order.

Русский

Если hf: IsMaxOn f s a и hg: MapsTo g t s и ha: g b = a, то IsMaxOn (f ∘ g) t b; это следует из двойственности порядка.

LaTeX

$$$hf : IsMaxOn f s a \;\; hg : MapsTo g t s \;\; ha : g b = a \Rightarrow IsMaxOn (f \circ g) t b$$$

Lean4

theorem comp_mapsTo {t : Set δ} {g : δ → α} {b : δ} (hf : IsMaxOn f s a) (hg : MapsTo g t s) (ha : g b = a) :
    IsMaxOn (f ∘ g) t b :=
  hf.dual.comp_mapsTo hg ha

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