comp_mapsTo — Mathlib

English

If hf: IsMinOn f s a and hg: MapsTo g t s and ha: g(b) = a, then IsMinOn (f ∘ g) t b.

Русский

Если hf: IsMinOn f s a и hg: MapsTo g t s и ha: g(b) = a, то IsMinOn (f ∘ g) t b.

LaTeX

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

Lean4

theorem comp_mapsTo {t : Set δ} {g : δ → α} {b : δ} (hf : IsMinOn f s a) (hg : MapsTo g t s) (ha : g b = a) :
    IsMinOn (f ∘ g) t b := fun y hy => by simpa only [ha, (· ∘ ·)] using hf (hg hy)

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