English
Let f: α → β, l a filter on α, and a ∈ α. If f has a minimum on l at the point g(b) for some g: δ → α and b ∈ δ, and g tends to l through l', then the composed function f ∘ g has a minimum on l' at b.
Русский
Пусть f: α → β, фильтр l на α, и некоторое a ∈ α. Если f достигает минимума на l в точке g(b) для некоторых g: δ → α и b ∈ δ, и g стремится к l через l', то композиция f ∘ g имеет минимум на l' в точке b.
LaTeX
$$$hf : IsMinFilter f l (g b) \rightarrow hg : Tendsto g l' l \rightarrow IsMinFilter (f \circ g) l' b$$$
Lean4
theorem comp_tendsto {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsMinFilter f l (g b)) (hg : Tendsto g l' l) :
IsMinFilter (f ∘ g) l' b :=
hg hf
