isConstant_comp — Mathlib

English

If f is constant with respect to l and g: β → γ, then g ∘ f is constant as a germ.

Русский

Если f является константой относительно l и g: β → γ, то композиция g ∘ f является константной зародышем.

LaTeX

$$$ (f : \mathrm{Germ}(l, \beta)).\text{IsConstant} \Rightarrow ((g \circ f) : \mathrm{Germ}(l, \gamma)).\text{IsConstant}$$$

Lean4

/-- If `f : α → β` is constant w.r.t. `l` and `g : β → γ`, then `g ∘ f : α → γ` also is. -/
theorem isConstant_comp {l : Filter α} {f : α → β} {g : β → γ} (h : (f : Germ l β).IsConstant) :
    ((g ∘ f) : Germ l γ).IsConstant := by
  obtain ⟨b, hb⟩ := h
  exact ⟨g b, hb.fun_comp g⟩

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