of_germ_isConstant — Mathlib

English

If every point x has a germ of f that is constant, then f is locally constant.

Русский

Если для каждого x гёрм функции f являются константами, то f является локально константной.

LaTeX

$$$\forall x, (f : \mathrm{Germ}(\mathcal N x) Y).IsConstant \Rightarrow \text{IsLocallyConstant } f$$$

Lean4

/-- If the germ of `f` w.r.t. each `𝓝 x` is constant, `f` is locally constant. -/
theorem of_germ_isConstant (h : ∀ x : X, (f : Germ (𝓝 x) Y).IsConstant) : IsLocallyConstant f :=
  by
  intro s
  rw [isOpen_iff_mem_nhds]
  intro a ha
  obtain ⟨b, hb⟩ := h a
  apply mem_of_superset hb
  intro x hx
  have : f x = f a := (mem_of_mem_nhds hb) ▸ hx
  rw [mem_preimage, this]
  exact ha

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